diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Contexts.ml | 4 | ||||
| -rw-r--r-- | src/Interpreter.ml | 1 | ||||
| -rw-r--r-- | src/InterpreterBorrows.ml | 3 | ||||
| -rw-r--r-- | src/InterpreterBorrowsCore.ml | 1 | ||||
| -rw-r--r-- | src/InterpreterExpansion.ml | 3 | ||||
| -rw-r--r-- | src/InterpreterProjectors.ml | 7 | ||||
| -rw-r--r-- | src/InterpreterUtils.ml | 4 | ||||
| -rw-r--r-- | src/Synthesis.ml | 2 |
8 files changed, 8 insertions, 17 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index f8a7b56b..0fe3a09a 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -27,8 +27,8 @@ let abstraction_id_counter, fresh_abstraction_id = AbstractionId.fresh_stateful_generator () (** We shouldn't need to reset the global counters, but it might be good to - to it from time to time, every time we evaluate/synthesize a function for - instance. + do it from time to time, for instance every time we start evaluating/ + synthesizing a function. The reasons are manifold: - it might prevent the counters from overflowing (although this seems diff --git a/src/Interpreter.ml b/src/Interpreter.ml index ec15093d..2789517e 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1,4 +1,3 @@ -open Errors module L = Logging module T = Types module A = CfimAst diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index a18ccefb..1dd4d247 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -3,7 +3,6 @@ module V = Values module C = Contexts module Subst = Substitute module L = Logging -open Utils open ValuesUtils open TypesUtils open InterpreterUtils @@ -226,7 +225,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) (* We sometimes need to reborrow values while giving a value back due: prepare that *) let allow_reborrows = true in let fresh_reborrow, apply_registered_reborrows = - prepare_reborrows config allow_reborrows ctx + prepare_reborrows config allow_reborrows in (* The visitor to give back the values *) let obj = diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml index 6e09c90c..bc2f5971 100644 --- a/src/InterpreterBorrowsCore.ml +++ b/src/InterpreterBorrowsCore.ml @@ -7,7 +7,6 @@ module V = Values module C = Contexts module Subst = Substitute module L = Logging -open Utils open InterpreterUtils (** TODO: cleanup this a bit, once we have a better understanding about diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index 2de06f24..345c3df3 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -10,7 +10,6 @@ module C = Contexts module Subst = Substitute module L = Logging open TypesUtils -open ValuesUtils module Inv = Invariants module S = Synthesis open InterpreterUtils @@ -54,7 +53,7 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config) let check_symbolic_no_ended = false in (* Prepare reborrows registration *) let fresh_reborrow, apply_registered_reborrows = - prepare_reborrows config allow_reborrows ctx + prepare_reborrows config allow_reborrows in (* Visitor to apply the expansion *) let obj = diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml index 3fa824ab..036082eb 100644 --- a/src/InterpreterProjectors.ml +++ b/src/InterpreterProjectors.ml @@ -5,8 +5,6 @@ module C = Contexts module Subst = Substitute module L = Logging open TypesUtils -open ValuesUtils -open Utils open InterpreterUtils open InterpreterBorrowsCore @@ -471,8 +469,7 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) - a function to apply the reborrows in a context Those functions are of course stateful. *) -let prepare_reborrows (config : C.config) (allow_reborrows : bool) - (ctx : C.eval_ctx) : +let prepare_reborrows (config : C.config) (allow_reborrows : bool) : (V.BorrowId.id -> V.BorrowId.id) * (C.eval_ctx -> C.eval_ctx) = let reborrows : (V.BorrowId.id * V.BorrowId.id) list ref = ref [] in (* The function to generate and register fresh reborrows *) @@ -502,7 +499,7 @@ let apply_proj_borrows_on_input_value (config : C.config) (ctx : C.eval_ctx) let allow_reborrows = true in (* Prepare the reborrows *) let fresh_reborrow, apply_registered_reborrows = - prepare_reborrows config allow_reborrows ctx + prepare_reborrows config allow_reborrows in (* Apply the projector *) let av = diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index 40ef0d05..5f86fec2 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -6,10 +6,8 @@ module E = Expressions module C = Contexts module Subst = Substitute module A = CfimAst -module L = Logging -open TypesUtils -open ValuesUtils open Utils +open TypesUtils (** Some utilities *) diff --git a/src/Synthesis.ml b/src/Synthesis.ml index 79fa4065..b0ecd554 100644 --- a/src/Synthesis.ml +++ b/src/Synthesis.ml @@ -71,4 +71,4 @@ let synthesize_function_call (_fid : A.fun_id) let synthesize_panic () : unit = () -let synthesize_assert (v : V.typed_value) : unit = () +let synthesize_assert (_v : V.typed_value) : unit = () |