From 464e2da5f51547e4350871431f1e9ad74c48094f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 8 Feb 2022 18:34:04 +0100
Subject: Update the Makefile to add hashmap as a test and fix some issues

---
 Makefile          |  8 +++++++-
 src/CfimOfJson.ml | 16 +++++++++++++++-
 src/Types.ml      |  8 ++++----
 3 files changed, 26 insertions(+), 6 deletions(-)

diff --git a/Makefile b/Makefile
index 0807e092..93ac5b2e 100644
--- a/Makefile
+++ b/Makefile
@@ -2,9 +2,13 @@ all: build-run-check-trace
 
 CHARON_HOME=../charon/charon
 CHARON_TESTS_DIR=$(CHARON_HOME)/tests/src
+DEST_DIR=tests/
+
 RS_TEST_FILE1=tests/src/no_nested_borrows.rs
 CFIM_TEST_FILE1=$(CHARON_TESTS_DIR)/no_nested_borrows.cfim
-DEST_DIR=tests/
+
+RS_TEST_FILE2=tests/src/hashmap.rs
+CFIM_TEST_FILE2=$(CHARON_TESTS_DIR)/hashmap.cfim
 
 # Build the project
 .PHONY: build
@@ -15,6 +19,7 @@ build:
 .PHONY: build-run
 build-run: build
 	dune exec -- src/main.exe $(CFIM_TEST_FILE1) -dest $(DEST_DIR) -test-units -test-trans-units > tests/trace_current.txt
+	dune exec -- src/main.exe $(CFIM_TEST_FILE2) -dest $(DEST_DIR)
 
 # Build the project and run the executable, then check that the behaviour
 # of the interpreter didn't change by comparing the newly generated trace
@@ -34,6 +39,7 @@ regen-trace: generate-cfim build-run
 .PHONY: generate-cfim
 generate-cfim:
 	cd ../charon/charon && cargo run $(RS_TEST_FILE1)
+	cd ../charon/charon && cargo run $(RS_TEST_FILE2)
 
 doc:
 	dune build @doc
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml
index c7bc4ce8..6cf7cf64 100644
--- a/src/CfimOfJson.ml
+++ b/src/CfimOfJson.ml
@@ -76,7 +76,11 @@ let ref_kind_of_json (js : json) : (T.ref_kind, string) result =
 
 let assumed_ty_of_json (js : json) : (T.assumed_ty, string) result =
   combine_error_msgs js "assumed_ty_of_json"
-    (match js with `String "Box" -> Ok T.Box | _ -> Error "")
+    (match js with
+    | `String "Box" -> Ok T.Box
+    | `String "Vec" -> Ok T.Vec
+    | `String "Option" -> Ok T.Option
+    | _ -> Error "")
 
 let type_id_of_json (js : json) : (T.type_id, string) result =
   combine_error_msgs js "type_id_of_json"
@@ -303,6 +307,9 @@ let field_proj_kind_of_json (js : json) : (E.field_proj_kind, string) result =
     | `Assoc [ ("ProjTuple", i) ] ->
         let* i = int_of_json i in
         Ok (E.ProjTuple i)
+    | `Assoc [ ("ProjOption", variant_id) ] ->
+        let* variant_id = T.VariantId.id_of_json variant_id in
+        Ok (E.ProjOption variant_id)
     | _ -> Error "")
 
 let projection_elem_of_json (js : json) : (E.projection_elem, string) result =
@@ -437,10 +444,17 @@ let rvalue_of_json (js : json) : (E.rvalue, string) result =
 
 let assumed_fun_id_of_json (js : json) : (A.assumed_fun_id, string) result =
   match js with
+  | `String "Replace" -> Ok A.Replace
   | `String "BoxNew" -> Ok A.BoxNew
   | `String "BoxDeref" -> Ok A.BoxDeref
   | `String "BoxDerefMut" -> Ok A.BoxDerefMut
   | `String "BoxFree" -> Ok A.BoxFree
+  | `String "VecNew" -> Ok A.VecNew
+  | `String "VecPush" -> Ok A.VecPush
+  | `String "VecInsert" -> Ok A.VecInsert
+  | `String "VecLen" -> Ok A.VecLen
+  | `String "VecIndex" -> Ok A.VecIndex
+  | `String "VecIndexMut" -> Ok A.VecIndexMut
   | _ -> Error ("assumed_fun_id_of_json failed on:" ^ show js)
 
 let fun_id_of_json (js : json) : (A.fun_id, string) result =
diff --git a/src/Types.ml b/src/Types.ml
index d7b9ab1b..9af97338 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -90,11 +90,11 @@ type ref_kind = Mut | Shared [@@deriving show, ord]
 
 type assumed_ty = Box | Vec | Option [@@deriving show, ord]
 
-(** The variant id for `Option::Some` *)
-let option_some_id = VariantId.of_int 0
-
 (** The variant id for `Option::None` *)
-let option_none_id = VariantId.of_int 1
+let option_none_id = VariantId.of_int 0
+
+(** The variant id for `Option::Some` *)
+let option_some_id = VariantId.of_int 1
 
 (** Type identifier for ADTs.
 
-- 
cgit v1.2.3