diff options
| -rw-r--r-- | src/LlbcOfJson.ml | 30 | ||||
| -rw-r--r-- | src/main.ml | 30 | ||||
| -rw-r--r-- | tests/misc/Constants.fst | 19 |
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 + |