From 05db1377f1b987050e58643b9bf001f62a77e303 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jan 2022 08:43:24 +0100
Subject: Introduce the type_context definition

---
 src/main.ml | 40 +++++++++++++++++++++++-----------------
 1 file changed, 23 insertions(+), 17 deletions(-)

(limited to 'src/main.ml')

diff --git a/src/main.ml b/src/main.ml
index 4616aadf..f2e6eb06 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -1,9 +1,11 @@
 open CfimOfJson
 open Logging
 open Print
+open Contexts
 module T = Types
 module A = CfimAst
 module I = Interpreter
+module C = Contexts
 
 type test = Test [@@deriving show]
 
@@ -13,31 +15,35 @@ let _ = show_test Test
  * reason, the -g option doesn't work *)
 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
-- 
cgit v1.2.3


From d7ac73c207461559f55623e8ff61d2bb7e5cf982 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jan 2022 08:44:10 +0100
Subject: Cleanup a bit

---
 src/main.ml | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'src/main.ml')

diff --git a/src/main.ml b/src/main.ml
index f2e6eb06..2d2518c7 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -1,15 +1,9 @@
 open CfimOfJson
 open Logging
 open Print
-open Contexts
 module T = Types
 module A = CfimAst
 module I = Interpreter
-module C = Contexts
-
-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 *)
-- 
cgit v1.2.3


From f2fb0dc39cfa9aef2b16963d3f8a270ec45bae5e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jan 2022 14:43:35 +0100
Subject: Make good progress on implementing utilities to test symbolic
 execution

---
 src/main.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/main.ml')

diff --git a/src/main.ml b/src/main.ml
index 2d2518c7..b4537c3a 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -46,4 +46,4 @@ let () =
       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
+      I.Test.test_unit_functions m.types m.functions
-- 
cgit v1.2.3


From ec40683d2462ae15c1d0e68dbf8c6e14825b9cef Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jan 2022 14:48:32 +0100
Subject: Implement tests for the symbolic interpreter

---
 src/main.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'src/main.ml')

diff --git a/src/main.ml b/src/main.ml
index b4537c3a..63f15c85 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -45,5 +45,8 @@ let () =
       (* Print the module *)
       log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m ^ "\n"));
 
-      (* Test the unit functions *)
-      I.Test.test_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_symbolic_functions m.types m.functions
-- 
cgit v1.2.3


From a263101a71d5be9d3f2a738527c2eedc850eb9ad Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jan 2022 15:10:41 +0100
Subject: Make minor modifications

---
 src/main.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/main.ml')

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
-- 
cgit v1.2.3