From edc2be164fcf53c333796e55b93f94bf6c9ed152 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Fri, 22 Jun 2018 19:03:02 +0100 Subject: 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. --- test/isabelle/Aarch64_code.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test/isabelle') 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 \ char \ (regstate, unit, exc bindS (write_mem_valS BC_bitU_list (bits_of_nat 8 (nat_of_char c))) (\_. returnS ()))" -definition "initial_state \ init_state initial_regstate (\seed. (False, seed)) 0" +definition "initial_state \ init_state initial_regstate" code_printing constant elf_entry \ (OCaml) "(Int'_of'_integer (Elf'_loader.elf'_entry _))" termination BigEndianReverse sorry -- cgit v1.2.3