implement assert, print

1 files changed, 24 insertions, 5 deletions

diff --git a/abstract/interpret.ml b/abstract/interpret.ml
index 51c7cd6..fe998a6 100644
--- a/abstract/interpret.ml
+++ b/abstract/interpret.ml
@@ -17,7 +17,14 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
 			E.meet (condition e1 env) (condition e2 env)
 		| AST_binary (AST_OR, e1, e2) ->
 			E.join (condition e1 env) (condition e2 env)
-		| _ -> env (* TODO : encode some transformations *)
+		(* transformations *)
+		| AST_unary (AST_NOT, (AST_binary(AST_AND, e1, e2), x)) ->
+			condition
+				(AST_binary(AST_OR, neg e1, neg e2), x) env
+		| AST_unary (AST_NOT, (AST_binary(AST_OR, e1, e2), x)) ->
+			condition
+				(AST_binary(AST_AND, neg e1, neg e2), x) env
+		| _ -> env (* TODO : encode some more transformations *)
 		end
 
 	let rec interp_stmt env stat =
@@ -39,19 +46,31 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
 			env
 		| AST_HALT -> E.bottom
 		| AST_assert (cond, l) ->
-			(* TODO *)
-			env
+			if not
+				(E.is_bot (condition (neg (cond, l)) env))
+			then begin
+				print_string (Abstract_syntax_printer.string_of_extent l);
+				print_string ": ERROR: assertion failure\n"
+			end;
+			condition (cond, l) env
 		| AST_print items ->
-			(* TODO *)
+			print_string (Abstract_syntax_printer.string_of_extent (snd stat));
+			print_string ": ";
+			print_string (E.var_str env (List.map fst items));
+			print_string "\n";
 			env
 		| _ -> assert false (* not implemented *)
 		end
 	
 	let interpret prog =
-		List.fold_left
+		let result = List.fold_left
 			(fun env x -> match x with
 				| AST_stat st -> interp_stmt env st
 				| _ -> env)
 			E.init
 			(fst prog)
+		in
+			print_string "Output: ";
+			print_string (E.all_vars_str result);
+			print_string "\n"
 end