summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--Makefile8
-rw-r--r--src/SymbolicToPure.ml15
2 files changed, 17 insertions, 6 deletions
diff --git a/Makefile b/Makefile
index 3c9d9f1e..e47a170d 100644
--- a/Makefile
+++ b/Makefile
@@ -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