added example

Isweet · May 1, 2017 · b9e28d2 · b9e28d2
1 parent a304f5c
commit b9e28d2
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 12 deletions.
diff --git a/Makefile b/Makefile
@@ -1,3 +1,5 @@
+SHELL := /bin/bash
+
 EXE_NAME  := symwhile
 TEST_NAME := mike_example
 
@@ -19,6 +21,6 @@ sanity_check:
 	which z3
 
 test: native
-	./$(EXE_NAME).native res/$(TEST_NAME).while
+	./$(EXE_NAME).native --semantics symbolic <(echo "input(x); input(y); assert not (y = 0); result := x / y")
 
 .PHONY: all clean native byte sanity
diff --git a/res/log_iterated_div.while b/res/log_iterated_div.while
diff --git a/src/symwhile.ml b/src/symwhile.ml
@@ -27,7 +27,7 @@ let main () =
                             | "symbolic" -> sem := Symbolic
                             | _          -> raise (Arg.Bad "--semantics (concrete|symbolic)")),
      "Choose semantics with which to run `while` stmt. (default = \"concrete\")");
-  ] (function s -> input := s) "usage: sym-while (<input file>|--)";
+  ] (function s -> input := s) "usage: sym-while <input file>";
 
   let chan = open_in !input in
   let lexbuf = Lexing.from_channel chan in