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