diff options
| -rw-r--r-- | Makefile | 8 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 15 |
2 files changed, 17 insertions, 6 deletions
@@ -18,16 +18,16 @@ build-run-check-trace: generate-cfim dune build src/main.exe && \ dune exec src/main.exe $(CFIM_TEST_FILE) > tests/trace_current.txt && \ cmp tests/trace_reference.txt tests/trace_current.txt && \ - cp fstar/Primitives.fst $(CHARON_TESTS_DIR) + cp fstar/Primitives.fst $(CHARON_TESTS_DIR) # Build the project and update the trace .PHONY: regen-trace regen-trace: generate-cfim dune build src/main.exe && \ dune exec src/main.exe $(CFIM_TEST_FILE) > tests/trace_current.txt && \ - rm -f tests/trace_reference.txt && \ - cp tests/trace_current.txt tests/trace_reference.txt \ - cp fstar/Primitives.fst $(CHARON_TESTS_DIR) + rm -f tests/trace_reference.txt && \ + cp tests/trace_current.txt tests/trace_reference.txt && \ + cp fstar/Primitives.fst $(CHARON_TESTS_DIR) .PHONY: generate-cfim generate-cfim: diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 52854c8b..faa95082 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -825,6 +825,16 @@ let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) : S.call * V.abs list = let abs_ancestors = list_ancestor_abstractions ctx abs in (call_info.forward, abs_ancestors) +(** Small utility. + + Return true if a function return type is monadic. + Always true, at the exception of some assumed functions. + *) +let fun_is_monadic (fun_id : A.fun_id) : bool = + match fun_id with + | A.Local _ -> true + | A.Assumed (A.BoxNew | BoxDeref | BoxDerefMut | BoxFree) -> false + let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = match e with | S.Return opt_v -> translate_return opt_v ctx @@ -892,7 +902,8 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : | S.Fun (fid, call_id) -> let ctx = bs_ctx_register_forward_call call_id call ctx in let func = Regular (fid, None) in - (ctx, func, true) + let monadic = fun_is_monadic fid in + (ctx, func, monadic) | S.Unop E.Not -> (ctx, Unop Not, false) | S.Unop E.Neg -> ( match args with @@ -1049,7 +1060,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) : (fun (arg, mp) -> mk_value_expression arg mp) (List.combine inputs args_mplaces) in - let monadic = true in + let monadic = fun_is_monadic fun_id in let call = { func; type_params; args } in let call_ty = mk_result_ty output.ty in let call = { e = Call call; ty = call_ty } in |