diff options
| author | Thomas Bauereiss | 2018-06-22 19:03:02 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-07-09 14:38:51 +0100 |
| commit | edc2be164fcf53c333796e55b93f94bf6c9ed152 (patch) | |
| tree | e1ac424b8d6ee3ca7a5264bd7067c06fba283c9d /test/isabelle | |
| parent | a6770dbaf3231a8a8050cea588eb186ab8b36a77 (diff) | |
Simplify treating of undefined_bool in Lem library
Use nondeterministic choice by default instead of a deterministic bitstream
generator in the state, which is slightly awkward to reason about, because
every use of undefined_boolS changes the state. The previous behaviour can be
implemented as Sail code, if desired.
Also add a default implementation of internal_pick that nondeterministically
chooses an element from a list.
Diffstat (limited to 'test/isabelle')
| -rw-r--r-- | test/isabelle/Aarch64_code.thy | 2 |
1 files changed, 1 insertions, 1 deletions
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 |