From 9f2f2340d5679dbd8219fdc7f026f80e1b3811c1 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 5 Jan 2022 14:35:12 +0100 Subject: Remove synthesize_set_discriminant --- src/Interpreter.ml | 1 - src/Synthesis.ml | 4 ---- 2 files changed, 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 = -- cgit v1.2.3