summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-28 00:22:42 +0100
committerSon Ho2022-01-28 00:22:42 +0100
commit60ab9675367059dd412e5935305f3005083b2533 (patch)
tree5d70065019c68bdf663bca532ef05a0c80d01df0
parent4eea9bc50c1f151f1b47f2b78327ce2fd92af300 (diff)
Make a minor cleaning
-rw-r--r--src/Translate.ml8
1 files changed, 0 insertions, 8 deletions
diff --git a/src/Translate.ml b/src/Translate.ml
index f8634225..1e8eb148 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -133,7 +133,6 @@ let translate_function_to_pure (config : C.partial_config)
(* We need to initialize the input/output variables *)
let module RegularFunIdMap = SymbolicToPure.RegularFunIdMap in
- let forward_sg = RegularFunIdMap.find (A.Local def_id, None) fun_sigs in
let forward_input_vars = CfimAstUtils.fun_def_get_input_vars fdef in
let forward_input_varnames =
List.map (fun (v : A.var) -> v.name) forward_input_vars
@@ -147,13 +146,6 @@ let translate_function_to_pure (config : C.partial_config)
{ ctx with forward_inputs }
in
- (* let forward_inputs =
- List.combine forward_input_varnames forward_sg.sg.inputs
- in
- let ctx, forward_inputs = SymbolicToPure.fresh_vars forward_inputs ctx in
-
- let ctx = { ctx with forward_inputs } in*)
-
(* Translate the forward function *)
let pure_forward =
SymbolicToPure.translate_fun_def