adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

autocorres: actually check results of type strengthening demo

This commit is contained in:
Japheth Lim 2016-06-30 01:12:28 +10:00
parent a933c6b7b7
commit b7c354f798
1 changed files with 24 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
tools/autocorres/tests/examples/type_strengthen_tricks.thy
View File

@ -44,6 +44,30 @@ thm opt_f'_def opt_g'_def opt_h'.simps opt_i'_def
thm opt_l'_def
thm st_f'_def st_g'_def st_h'_def st_i'.simps (* hax'_def *)
thm exc_f'_def
(* Check the above claims. *)
term "pure_f' :: lifted_globals \<Rightarrow> unit option"
term "pure_f2' :: lifted_globals \<Rightarrow> unit option"
term "pure_g' :: ure_C ptr \<Rightarrow> ure_C ptr"
term "pure_h' :: ure_C ptr \<Rightarrow> int"
term "pure_i' :: int \<Rightarrow> int"
term "pure_j' :: ure_C \<Rightarrow> int"
term "pure_k' :: ure_C \<Rightarrow> int"
term "pure_div_roundup' :: word32 \<Rightarrow> word32 \<Rightarrow> word32"
term "gets_f' :: lifted_globals \<Rightarrow> word32 option"
term "gets_g' :: lifted_globals \<Rightarrow> word32 option"
term "opt_f' :: word32 ptr \<Rightarrow> lifted_globals \<Rightarrow> word32 option"
term "opt_g' :: int \<Rightarrow> lifted_globals \<Rightarrow> int option"
term "opt_h' :: nat \<Rightarrow> ure_C ptr \<Rightarrow> lifted_globals \<Rightarrow> word32 option"
term "opt_i' :: (lifted_globals, int) nondet_monad"
term "opt_j' :: ure_C ptr \<Rightarrow> ure_C ptr \<Rightarrow> lifted_globals \<Rightarrow> int option"
term "opt_a' :: nat \<Rightarrow> word32 \<Rightarrow> word32 \<Rightarrow> lifted_globals \<Rightarrow> word32 option"
term "opt_l' :: word32 \<Rightarrow> (lifted_globals, word32) nondet_monad"
term "st_f' :: ure_C ptr \<Rightarrow> ure_C ptr \<Rightarrow> (lifted_globals, unit) nondet_monad"
term "st_g' :: word32 ptr \<Rightarrow> (lifted_globals, word32) nondet_monad"
term "st_h' :: word32 \<Rightarrow> (lifted_globals, word32) nondet_monad"
term "st_i' :: nat \<Rightarrow> ure_C ptr \<Rightarrow> ure_C ptr \<Rightarrow> (lifted_globals, ure_C ptr) nondet_monad"
term "exc_f' :: word8 ptr \<Rightarrow> 32 signed word ptr \<Rightarrow> (lifted_globals, int) nondet_monad"
end
end