diff options
| -rw-r--r-- | Makefile | 8 | ||||
| -rw-r--r-- | src/CfimOfJson.ml | 16 | ||||
| -rw-r--r-- | src/Types.ml | 8 |
3 files changed, 26 insertions, 6 deletions
@@ -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. |