1open HolKernel bossLib
2
3val _ = loadPath :=
4            (concat [Globals.HOLDIR, "/examples/separationLogic/src"]) ::
5            (concat [Globals.HOLDIR, "/examples/separationLogic/src/holfoot"]) ::
6            !loadPath;
7
8val _ = map load ["holfootParser", "holfoot_pp_print", "holfootLib"];
9open holfootParser;
10open holfoot_pp_print;
11open holfootLib;
12
13open separationLogicTheory vars_as_resourceTheory holfootTheory generalHelpersTheory;
14
15val hard_fail = true;
16val quiet = true;
17val _ = Parse.current_backend := PPBackEnd.vt100_terminal;
18val examples_dir = concat [Globals.HOLDIR, "/examples/separationLogic/src/holfoot/EXAMPLES/automatic/"];
19
20(* For manual
21
22val hard_fail = false;
23val _ = Parse.current_backend := PPBackEnd.emacs_terminal;
24val quiet = true
25*)
26
27fun test_file file = let
28  open PPBackEnd Parse
29  val ok = snd ((holfootLib.holfoot_interactive_verify_spec (not quiet) (not quiet) (concat [examples_dir, file]) (SOME [generate_vcs]) []));
30  val _ = print "\n";
31  val _ = if (not ok andalso hard_fail) then Process.exit Process.failure else ();
32in ok end
33
34val _ = test_file "append-parkinson.dsf";
35val _ = test_file "append-parkinson.sf";
36val _ = test_file "append-unroll.dsf";
37val _ = test_file "append.dsf";
38val _ = test_file "append.dsf2";
39val _ = test_file "append.sf";
40val _ = test_file "array_copy-shape.dsf";
41val _ = test_file "assert-dispose.dsf";
42(* val _ = test_file "binary_search-shape.dsf"; *)
43val _ = test_file "business1.sf";
44val _ = test_file "copy.dsf";
45val _ = test_file "copy.dsf2";
46val _ = test_file "copy.sf";
47val _ = test_file "entailments.ent";
48val _ = test_file "filter.sf";
49val _ = test_file "filter_rec-gen.dsf";
50val _ = test_file "filter_rec.dsf";
51val _ = test_file "list.sf";
52val _ = test_file "list_alloc_dealloc_length.dsf";
53val _ = test_file "list_length.dsf";
54val _ = test_file "list_length.sf";
55val _ = test_file "list_length_iter.dsf";
56val _ = test_file "list_length_iter.dsf2";
57val _ = test_file "list_length_iter.sf";
58val _ = test_file "memory_manager.sf";
59val _ = test_file "mergesort.sf";
60val _ = test_file "mm_buf.sf";
61val _ = test_file "mm_non_blocking.sf";
62val _ = test_file "parallel_mergesort.sf";
63val _ = test_file "parallel_tree_deallocate.sf";
64val _ = test_file "passive_stack_race.sf";
65val _ = test_file "pointer_non_transferring_buffer.sf";
66val _ = test_file "pointer_transferring_buffer.sf";
67val _ = test_file "queue.dsf";
68val _ = test_file "queue.sf";
69val _ = test_file "quicksort-shape.dsf";
70val _ = test_file "remove.sf";
71val _ = test_file "reverse-parkinson.dsf";
72val _ = test_file "reverse-parkinson.sf";
73val _ = test_file "reverse.dsf";
74val _ = test_file "reverse.dsf2";
75val _ = test_file "reverse.sf";
76val _ = test_file "split_binary_semaphore.sf";
77val _ = test_file "tree.sf";
78val _ = test_file "tree_copy.dsf";
79
80val _ = Process.exit Process.success;
81