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

autocorres: fix up remaining failures in test suite (all typo level)

This commit is contained in:
Japheth Lim 2016-06-30 09:57:23 +10:00
parent 162a2266a1
commit 0afb748b1b
3 changed files with 9 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
tools/autocorres/tests/examples/FunctionInfoDemo.thy
View File

@ -28,8 +28,8 @@ text \<open>
3. Function: Each function that is processed in a given phase.
\<close>
ML \<open>
val file_info: FunctionInfo2.function_info Symtab.table FunctionInfo2.Phasetab.table =
the (Symtab.lookup (AutoCorresFunctionInfo2.get @{theory}) "function_info.c")
val file_info: FunctionInfo.function_info Symtab.table FunctionInfo.Phasetab.table =
the (Symtab.lookup (AutoCorresFunctionInfo.get @{theory}) "function_info.c")
\<close>
text \<open>
@ -37,7 +37,7 @@ text \<open>
This shows the final definition of each function in file_info:
\<close>
ML \<open>
the (FunctionInfo2.Phasetab.lookup file_info FunctionInfo2.TS) |> Symtab.dest |> map snd
the (FunctionInfo.Phasetab.lookup file_info FunctionInfo.TS) |> Symtab.dest |> map snd
|> app (fn f_info => writeln ("Definition of " ^ #name f_info ^ ":\n" ^
Syntax.string_of_term @{context}
(Thm.prop_of (#definition f_info))))
@ -55,12 +55,12 @@ text \<open>
\<close>
ML \<open>
let
val other_phases = [FunctionInfo2.CP, FunctionInfo2.L1, FunctionInfo2.L2, FunctionInfo2.HL, FunctionInfo2.WA];
val other_phases = [FunctionInfo.CP, FunctionInfo.L1, FunctionInfo.L2, FunctionInfo.HL, FunctionInfo.WA];
fun get_def_at f phase =
the (FunctionInfo2.Phasetab.lookup file_info phase)
the (FunctionInfo.Phasetab.lookup file_info phase)
|> (fn phase_info => #definition (the (Symtab.lookup phase_info f)));
in
the (FunctionInfo2.Phasetab.lookup file_info FunctionInfo2.TS) |> Symtab.dest |> map fst
the (FunctionInfo.Phasetab.lookup file_info FunctionInfo.TS) |> Symtab.dest |> map fst
|> app (fn f_name =>
writeln ("Intermediate definitions of " ^ f_name ^ ":\n" ^
String.concat (map (fn phase =>

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

@ -62,7 +62,7 @@ term "opt_h' :: nat \<Rightarrow> ure_C ptr \<Rightarrow> lifted_globals \<Right
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_a2' :: word32 \<Rightarrow> lifted_globals \<Rightarrow> word32 option"
term "opt_a2' :: word32 \<Rightarrow> (lifted_globals, word32) nondet_monad"
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"

4
tools/autocorres/tests/proof-tests/skip_heap_abs.thy
View File

@ -18,8 +18,8 @@ autocorres [skip_heap_abs] "skip_heap_abs.c"
(* There should be no heap lift phase. *)
ML {*
val fn_infos = the (Symtab.lookup (AutoCorresFunctionInfo2.get @{theory}) "skip_heap_abs.c");
assert (is_none (FunctionInfo2.Phasetab.lookup fn_infos FunctionInfo2.HL)) "skip_heap_abs failed";
val fn_infos = the (Symtab.lookup (AutoCorresFunctionInfo.get @{theory}) "skip_heap_abs.c");
assert (is_none (FunctionInfo.Phasetab.lookup fn_infos FunctionInfo.HL)) "skip_heap_abs failed";
*}
end