diff options
| author | Thomas Bauereiss | 2018-07-07 22:47:57 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-07-09 14:47:49 +0100 |
| commit | 5d862dc23d4641a0e7d89cd747bc2ba4007ee8f5 (patch) | |
| tree | b3c5d3e5d903593db97d03c79f8ad0ad6cc89a27 /test | |
| parent | 2529f5a65d70dfffe40ead73ae49aaa4d78fefb4 (diff) | |
Update CHERI code generation from Isabelle
Diffstat (limited to 'test')
| -rw-r--r-- | test/isabelle/Cheri_code.thy | 2 | ||||
| -rw-r--r-- | test/isabelle/run_cheri.ml | 8 |
2 files changed, 5 insertions, 5 deletions
diff --git a/test/isabelle/Cheri_code.thy b/test/isabelle/Cheri_code.thy index cfd01413..13884ad5 100644 --- a/test/isabelle/Cheri_code.thy +++ b/test/isabelle/Cheri_code.thy @@ -50,7 +50,7 @@ fun write_char_mem :: "int \<Rightarrow> char \<Rightarrow> (regstate, unit, exc bindS (write_mem_valS BC_bitU_list (bits_of_nat 8 (nat_of_char c))) (\<lambda>_. returnS ()))" -definition "initial_state \<equiv> init_state initial_regstate (\<lambda>seed. (False, seed)) 0" +definition "initial_state \<equiv> init_state initial_regstate" code_printing constant elf_entry \<rightharpoonup> (OCaml) "(Arith.Int'_of'_integer (Elf'_loader.elf'_entry _))" code_printing constant get_time_ns \<rightharpoonup> (OCaml) "(Arith.Int'_of'_integer (Big'_int.big'_int'_of'_int (Pervasives.int'_of'_float (1e9 *. Unix.gettimeofday _))))" diff --git a/test/isabelle/run_cheri.ml b/test/isabelle/run_cheri.ml index f51ef4dd..283e4283 100644 --- a/test/isabelle/run_cheri.ml +++ b/test/isabelle/run_cheri.ml @@ -63,8 +63,8 @@ let usage_msg = "Sail OCaml RTS options:" let () = Arg.parse options (fun s -> opt_file_arguments := !opt_file_arguments @ [s]) usage_msg -let (>>) = State_monad.bindS -let liftS = State_lifting.liftState (Cheri_types.get_regval, Cheri_types.set_regval) +let (>>) = Sail2_state_monad.bindS +let liftS = Sail2_state_lifting.liftState (Cheri_types.get_regval, Cheri_types.set_regval) let load_elf_segment seg = let open Elf_interpreted_segment in @@ -78,7 +78,7 @@ let load_elf_segment seg = prerr_endline ("Segment base address: " ^ Big_int.string_of_big_int base); prerr_endline ("Segment physical address: " ^ Big_int.string_of_big_int paddr); print_segment seg; - State.iteriS writer (Byte_sequence.char_list_of_byte_sequence bs) + Sail2_state.iteriS writer (Byte_sequence.char_list_of_byte_sequence bs) let _ = Random.self_init (); @@ -88,5 +88,5 @@ let _ = in (* State_monad.prerr_results *) (Cheri_code.initial_state |> - (State.iterS load_elf_segment elf_segments >> (fun _ -> + (Sail2_state.iterS load_elf_segment elf_segments >> (fun _ -> liftS (Cheri.main ())))); |