summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-05 14:35:12 +0100
committerSon Ho2022-01-05 14:35:12 +0100
commit9f2f2340d5679dbd8219fdc7f026f80e1b3811c1 (patch)
tree0c0fa0dfab48ae0a70912fad083b3f5bd065feaa /src
parent57a019c4b18d4f9a695f4520dd33d482abde3d5f (diff)
Remove synthesize_set_discriminant
Diffstat (limited to 'src')
-rw-r--r--src/Interpreter.ml1
-rw-r--r--src/Synthesis.ml4
2 files changed, 0 insertions, 5 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 970ef3a6..482a3623 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -3521,7 +3521,6 @@ let rec end_loan_exactly_at_place (config : C.config) (access : access_kind)
*)
let set_discriminant (config : C.config) (ctx : C.eval_ctx) (p : E.place)
(variant_id : T.VariantId.id) : C.eval_ctx * statement_eval_res =
- S.synthesize_set_discriminant p variant_id;
(* Access the value *)
let access = Write in
let ctx = update_ctx_along_read_place config access p ctx in
diff --git a/src/Synthesis.ml b/src/Synthesis.ml
index 51aa0882..dce40470 100644
--- a/src/Synthesis.ml
+++ b/src/Synthesis.ml
@@ -63,10 +63,6 @@ let synthesize_eval_rvalue_aggregate (aggregate_kind : E.aggregate_kind)
(ops : E.operand list) : unit =
()
-let synthesize_set_discriminant (p : E.place) (variant_id : T.VariantId.id) :
- unit =
- ()
-
let synthesize_non_local_function_call (fid : A.assumed_fun_id)
(region_params : T.erased_region list) (type_params : T.ety list)
(args : E.operand list) (dest : E.place) : unit =