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

WIP: autocorres: more incremental translation fixes; update a testcase

This commit is contained in:
Japheth Lim 2016-06-29 23:37:51 +10:00
parent 1181b9bc1f
commit b8a1743148
2 changed files with 7 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
tools/autocorres/autocorres.ML
View File

@ -629,8 +629,10 @@ let
(* Collect final translation results. *)
val l1_info = FSeq.list_of l1_results |> map snd |> Utils.symtab_merge false;
val l2_info = FSeq.list_of l2_results |> map snd |> Utils.symtab_merge false;
val hl_info = FSeq.list_of hl_results |> map snd |> Utils.symtab_merge false;
val wa_info = FSeq.list_of wa_results |> map snd |> Utils.symtab_merge false;
val hl_info = if skip_heap_abs then Symtab.empty else
FSeq.list_of hl_results |> map snd |> Utils.symtab_merge false;
val wa_info = if skip_word_abs then Symtab.empty else
FSeq.list_of wa_results |> map snd |> Utils.symtab_merge false;
val ts_results' = FSeq.list_of ts_results;
val ts_info = ts_results' |> map snd |> Utils.symtab_merge false;

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

@ -16,9 +16,10 @@ theory skip_heap_abs imports "../../AutoCorres" begin
install_C_file "skip_heap_abs.c"
autocorres [skip_heap_abs] "skip_heap_abs.c"
(* There should be no heap lift theorem. *)
(* There should be no heap lift phase. *)
ML {*
assert (is_none (AutoCorresData.get_thm @{theory} "skip_heap_abs.c" "HL" "f")) "skip_heap_abs failed"
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";
*}
end