adapt to new LLBC (without OperandConstantValue)

3 files changed, 46 insertions, 33 deletions

diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml
index a074ed1e..3ff45077 100644
--- a/src/LlbcOfJson.ml
+++ b/src/LlbcOfJson.ml
@@ -381,24 +381,18 @@ let binop_of_json (js : json) : (E.binop, string) result =
 let constant_value_of_json (js : json) : (V.constant_value, string) result =
   combine_error_msgs js "constant_value_of_json"
     (match js with
-    (* This indirection is because Charon still export the type OperandConstantValue,
-      * which had other variants than ConstantValue before.
-      *)
-    | `Assoc [ ("ConstantValue", `List [ cv ]) ] ->
-        (match cv with
-          | `Assoc [ ("Scalar", scalar_value) ] ->
-              let* scalar_value = scalar_value_of_json scalar_value in
-              Ok (V.Scalar scalar_value)
-          | `Assoc [ ("Bool", v) ] ->
-              let* v = bool_of_json v in
-              Ok (V.Bool v)
-          | `Assoc [ ("Char", v) ] ->
-              let* v = char_of_json v in
-              Ok (V.Char v)
-          | `Assoc [ ("String", v) ] ->
-              let* v = string_of_json v in
-              Ok (V.String v)
-          | _ -> Error "")
+    | `Assoc [ ("Scalar", scalar_value) ] ->
+        let* scalar_value = scalar_value_of_json scalar_value in
+        Ok (V.Scalar scalar_value)
+    | `Assoc [ ("Bool", v) ] ->
+        let* v = bool_of_json v in
+        Ok (V.Bool v)
+    | `Assoc [ ("Char", v) ] ->
+        let* v = char_of_json v in
+        Ok (V.Char v)
+    | `Assoc [ ("String", v) ] ->
+        let* v = string_of_json v in
+        Ok (V.String v)
     | _ -> Error "")
   
 let operand_of_json (js : json) : (E.operand, string) result =
diff --git a/src/main.ml b/src/main.ml
index 93b094fd..6b1083f5 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -124,21 +124,21 @@ let () =
    * command-line arguments *)
   (* By setting a level for the main_logger_handler, we filter everything *)
   Easy_logging.Handlers.set_level main_logger_handler EL.Debug;
-  main_log#set_level EL.Debug;
-  llbc_of_json_logger#set_level EL.Debug;
-  pre_passes_log#set_level EL.Debug;
-  interpreter_log#set_level EL.Debug;
-  statements_log#set_level EL.Debug;
-  paths_log#set_level EL.Debug;
-  expressions_log#set_level EL.Debug;
-  expansion_log#set_level EL.Debug;
-  borrows_log#set_level EL.Debug;
-  invariants_log#set_level EL.Debug;
-  pure_utils_log#set_level EL.Debug;
-  symbolic_to_pure_log#set_level EL.Debug;
-  pure_micro_passes_log#set_level EL.Debug;
-  pure_to_extract_log#set_level EL.Debug;
-  translate_log#set_level EL.Debug;
+  main_log#set_level EL.Info;
+  llbc_of_json_logger#set_level EL.Info;
+  pre_passes_log#set_level EL.Info;
+  interpreter_log#set_level EL.Info;
+  statements_log#set_level EL.Info;
+  paths_log#set_level EL.Info;
+  expressions_log#set_level EL.Info;
+  expansion_log#set_level EL.Info;
+  borrows_log#set_level EL.Info;
+  invariants_log#set_level EL.Info;
+  pure_utils_log#set_level EL.Info;
+  symbolic_to_pure_log#set_level EL.Info;
+  pure_micro_passes_log#set_level EL.Info;
+  pure_to_extract_log#set_level EL.Info;
+  translate_log#set_level EL.Info;
   (* Load the module *)
   let json = Yojson.Basic.from_file filename in
   match llbc_module_of_json json with
diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst
index 9611c778..28a9ace7 100644
--- a/tests/misc/Constants.fst
+++ b/tests/misc/Constants.fst
@@ -117,3 +117,22 @@ let get_z2_fwd : result i32 =
     end
   end
 
+(** [constants::S1] *)
+let s1_fwd : result u32 = Return 6
+
+(** [constants::S2] *)
+let s2_fwd : result u32 =
+  begin match s1_fwd with
+  | Fail -> Fail
+  | Return i ->
+    begin match incr_fwd i with | Fail -> Fail | Return i0 -> Return i0 end
+  end
+
+(** [constants::S3] *)
+let s3_fwd : result (pair_t u32 u32) =
+  begin match p3_fwd with | Fail -> Fail | Return p -> Return p end
+
+(** [constants::S4] *)
+let s4_fwd : result (pair_t u32 u32) =
+  begin match mk_pair1_fwd 7 8 with | Fail -> Fail | Return p -> Return p end
+