Merge remote-tracking branch 'refs/remotes/origin/main'

1 files changed, 26 insertions, 23 deletions

diff --git a/src/main.ml b/src/main.ml
index 546f09a8..ac49b782 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -5,40 +5,40 @@ module T = Types
 module A = CfimAst
 module I = Interpreter
 
-type test = Test [@@deriving show]
-
-let _ = show_test Test
-
 (* This is necessary to have a backtrace when raising exceptions - for some
  * reason, the -g option doesn't work.
  * JP: are you running with OCAMLRUNPARAM=b=1? *)
 let () = Printexc.record_backtrace true
 
-let usage = Printf.sprintf {|Aenaes: verification of Rust programs by translation
+let usage =
+  Printf.sprintf
+    {|Aenaes: verification of Rust programs by translation
 
 Usage: %s [OPTIONS] FILE
-|} Sys.argv.(0);;
+|}
+    Sys.argv.(0)
 
 let () =
-  let spec = [
-  ] in
+  let spec = [] in
   let spec = Arg.align spec in
   let filename = ref "" in
-  let fail () = print_string usage; exit 1 in
-  Arg.parse spec (fun f ->
-    if not (Filename.check_suffix f ".cfim") then begin
-      print_string "Unrecognized file extension";
-      fail ()
-    end else if not (Sys.file_exists f) then begin
-      print_string "File not found";
-      fail ()
-    end else
-      filename := f
-  ) usage;
-  if !filename = "" then begin
+  let fail () =
     print_string usage;
     exit 1
-  end;
+  in
+  Arg.parse spec
+    (fun f ->
+      if not (Filename.check_suffix f ".cfim") then (
+        print_string "Unrecognized file extension";
+        fail ())
+      else if not (Sys.file_exists f) then (
+        print_string "File not found";
+        fail ())
+      else filename := f)
+    usage;
+  if !filename = "" then (
+    print_string usage;
+    exit 1);
   let json = Yojson.Basic.from_file !filename in
   match cfim_module_of_json json with
   | Error s -> log#error "error: %s\n" s
@@ -46,5 +46,8 @@ let () =
       (* Print the module *)
       log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m ^ "\n"));
 
-      (* Test the unit functions *)
-      I.Test.test_all_unit_functions m.types m.functions
+      (* Test the unit functions with the concrete interpreter *)
+      I.Test.test_unit_functions m.types m.functions;
+
+      (* Evaluate the symbolic interpreter on the functions *)
+      I.Test.test_functions_symbolic m.types m.functions