Make minor modifications

4 files changed, 23 insertions, 13 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 523957af..c8739394 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -162,7 +162,7 @@ module Test = struct
     List.iter test_unit_fun unit_funs
 
   (** Execute the symbolic interpreter on a function. *)
-  let test_symbolic_function (type_context : C.type_context)
+  let test_function_symbolic (type_context : C.type_context)
       (fun_defs : A.fun_def list) (fid : A.FunDefId.id) :
       C.eval_ctx eval_result list =
     (* Retrieve the function declaration *)
@@ -171,7 +171,7 @@ module Test = struct
     (* Debug *)
     L.log#ldebug
       (lazy
-        ("test_symbolic_function: " ^ Print.Types.name_to_string fdef.A.name));
+        ("test_function_symbolic: " ^ Print.Types.name_to_string fdef.A.name));
 
     (* Create the evaluation context *)
     let ctx = initialize_symbolic_context_for_fun type_context fun_defs fdef in
@@ -185,16 +185,18 @@ module Test = struct
       TODO: for now we ignore the functions which contain loops, because
       they are not supported by the symbolic interpreter.
    *)
-  let test_symbolic_functions (type_defs : T.type_def list)
+  let test_functions_symbolic (type_defs : T.type_def list)
       (fun_defs : A.fun_def list) : unit =
     let no_loop_funs =
       List.filter (fun f -> not (CfimAstUtils.fun_def_has_loops f)) fun_defs
     in
     let test_fun (def : A.fun_def) : unit =
       let type_ctx = { C.type_defs } in
-      let res = test_symbolic_function type_ctx fun_defs def.A.def_id in
-      if List.for_all Result.is_ok res then ()
-      else failwith "Unit test failed (symbolic execution)"
+      (* Execute the function - note that as the symbolic interpreter explores
+       * all the path, some executions are expected to "panic": we thus don't
+       * check the return value *)
+      let _ = test_function_symbolic type_ctx fun_defs def.A.def_id in
+      ()
     in
     List.iter test_fun no_loop_funs
 end
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 114f0daf..83d531a0 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -475,8 +475,9 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
   (* Debugging *)
   L.log#ldebug
     (lazy
-      ("\n" ^ eval_ctx_to_string ctx ^ "\nAbout to evaluate statement: "
-     ^ statement_to_string ctx st ^ "\n"));
+      ("\n**About to evaluate statement**: [\n"
+      ^ statement_to_string_with_tab ctx st
+      ^ "\n]\n\n**Context**:\n" ^ eval_ctx_to_string ctx ^ "\n\n"));
   (* Sanity check *)
   if config.C.check_invariants then Inv.check_invariants ctx;
   (* Evaluate *)
@@ -504,7 +505,7 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
       match v.value with
       | Concrete (Bool b) ->
           if b = assertion.expected then [ Ok (ctx, Unit) ] else [ Error Panic ]
-      | _ -> failwith "Expected a boolean")
+      | _ -> failwith ("Expected a boolean, got: " ^ V.show_value v.value))
   | A.Call call -> eval_function_call config ctx call
   | A.Panic -> [ Error Panic ]
   | A.Return -> [ Ok (ctx, Return) ]
@@ -611,9 +612,9 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets)
             eval_statement config ctx st
           in
           (* Execute the two branches *)
-          List.append
-            (expand_and_execute see_true st1)
-            (expand_and_execute see_false st2)
+          let ctxl_true = expand_and_execute see_true st1 in
+          let ctxl_false = expand_and_execute see_false st2 in
+          List.append ctxl_true ctxl_false
       | _ -> failwith "Inconsistent state")
   | A.SwitchInt (int_ty, tgts, otherwise) -> (
       match op_v.value with
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index cc54cd24..9f6cf495 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -26,6 +26,9 @@ let operand_to_string = Print.EvalCtxCfimAst.operand_to_string
 let statement_to_string ctx =
   Print.EvalCtxCfimAst.statement_to_string ctx "" "  "
 
+let statement_to_string_with_tab ctx =
+  Print.EvalCtxCfimAst.statement_to_string ctx "  " "  "
+
 let same_symbolic_id (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) : bool =
   sv0.V.sv_id = sv1.V.sv_id
 
@@ -65,6 +68,10 @@ let mk_typed_value_from_proj_comp (sv : V.symbolic_proj_comp) : V.typed_value =
   let value = V.Symbolic sv in
   { V.value; ty }
 
+(** Create a typed value from a symbolic value.
+
+    Initializes the set of ended regions with `empty`.
+ *)
 let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) :
     V.typed_value =
   let spc = { V.svalue; rset_ended = T.RegionId.Set.empty } in
diff --git a/src/main.ml b/src/main.ml
index 63f15c85..e5c3c324 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -49,4 +49,4 @@ let () =
       I.Test.test_unit_functions m.types m.functions;
 
       (* Evaluate the symbolic interpreter on the functions *)
-      I.Test.test_symbolic_functions m.types m.functions
+      I.Test.test_functions_symbolic m.types m.functions