autocorres: update to Isabelle2020

Signed-off-by: Gerwin Klein <[email protected]>
Xaphiosis · Oct 27, 2020 · 82e116e · 82e116e
1 parent 1842825
commit 82e116e
Show file tree

Hide file tree

Showing 4 changed files with 3 additions and 2 deletions.
diff --git a/tools/autocorres/Makefile b/tools/autocorres/Makefile
@@ -26,7 +26,7 @@ ALL_TESTS_THY := $(PARSE_TESTS_THY) $(PROOF_TESTS_THY) $(EXAMPLES_THY)
 # Generate an Isabelle "ROOT" file containing all of our test cases.
 tests/ROOT: $(ALL_TESTS_C) $(ALL_TESTS_THY) ../../misc/scripts/gen_isabelle_root.py
 	python3 ../../misc/scripts/gen_isabelle_root.py -o $@ -b AutoCorres -s AutoCorresTest -d HOL-Number_Theory \
-		-i tests/parse-tests -i tests/proof-tests -i tests/examples --quick-and-dirty
+		-i tests/parse-tests -i tests/proof-tests -i tests/examples --quick-and-dirty --dir parse-tests --dir proof-tests --dir examples
 
 # Generate a Isabelle "All.thy" file containing imports to all the test cases.
 tests/All.thy: $(ALL_TESTS_C) $(ALL_TESTS_THY) ../../misc/scripts/gen_isabelle_root.py

diff --git a/tools/autocorres/ROOT b/tools/autocorres/ROOT
@@ -14,6 +14,7 @@ session AutoCorres = CParser +
     Lib
     CLib
   theories
+    "DataStructures"
     "AutoCorres"
 
 session AutoCorresSEL4 in "test-seL4" = CBaseRefine +

diff --git a/tools/autocorres/tests/examples/BinarySearch.thy b/tools/autocorres/tests/examples/BinarySearch.thy
@@ -5,7 +5,7 @@
  *)
 
 theory BinarySearch
-imports "AutoCorres.AutoCorres" "../../DataStructures"
+imports "AutoCorres.AutoCorres" "AutoCorres.DataStructures"
 begin
 
 external_file "binary_search.c"

diff --git a/tools/autocorres/tests/parse-tests/simple.c → tools/autocorres/tests/parse-tests/basic.c b/tools/autocorres/tests/parse-tests/simple.c → tools/autocorres/tests/parse-tests/basic.c