diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/builtins/test_extras.lem | 3 | ||||
| -rw-r--r-- | test/hol/test_raw_addScript.sml | 6 | ||||
| -rw-r--r-- | test/isabelle/Aarch64_code.thy | 2 |
3 files changed, 4 insertions, 7 deletions
diff --git a/test/builtins/test_extras.lem b/test/builtins/test_extras.lem index 136f680e..ae3ed1ba 100644 --- a/test/builtins/test_extras.lem +++ b/test/builtins/test_extras.lem @@ -17,6 +17,3 @@ let undefined_bitvector len = return (zeros(len)) val undefined_unit : forall 'rv 'e. unit -> monad 'rv unit 'e let undefined_unit () = return () - -val internal_pick : forall 'rv 'a 'e. list 'a -> monad 'rv 'a 'e -let internal_pick xs = return (List_extra.head xs) diff --git a/test/hol/test_raw_addScript.sml b/test/hol/test_raw_addScript.sml index 1eb90ef8..20465eb2 100644 --- a/test/hol/test_raw_addScript.sml +++ b/test/hol/test_raw_addScript.sml @@ -783,7 +783,7 @@ val () = computeLib.extend_compset [ ] ] cs; -val empty_state = ``init_state initial_regstate bool_oracle seed``; +val empty_state = ``init_state initial_regstate``; val init_registers_result = ``init_registers vinitPC s`` @@ -927,7 +927,7 @@ install_code_result val test_raw_add_thm = Q.store_thm("test_raw_add_thm", `PrePost - (λs. s = init_state initial_regstate bool_oracle seed) + (λs. s = init_state initial_regstate) (install_and_run test_raw_add_insts 40) (λ_ s. test_raw_add_post s)`, rw[PrePost_def] @@ -1378,7 +1378,7 @@ computeLib.CBV_CONV cs ``decode (EL 1 test_raw_add_insts)`` val th1 = EVAL ``THE (decode (EL 1 test_raw_add_insts))`` -val s1 = EVAL ``init_cp0_state () (init_state (regs:regstate) o1 seed)`` +val s1 = EVAL ``init_cp0_state () (init_state (regs:regstate))`` val th2 = ``execute ^(rhs(concl th1)) ^s1`` |> SIMP_CONV(srw_ss())[execute_def] diff --git a/test/isabelle/Aarch64_code.thy b/test/isabelle/Aarch64_code.thy index 05e5bb2e..8a0e1795 100644 --- a/test/isabelle/Aarch64_code.thy +++ b/test/isabelle/Aarch64_code.thy @@ -52,7 +52,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) "(Int'_of'_integer (Elf'_loader.elf'_entry _))" termination BigEndianReverse sorry |