summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/Contexts.ml4
-rw-r--r--src/Interpreter.ml1
-rw-r--r--src/InterpreterBorrows.ml3
-rw-r--r--src/InterpreterBorrowsCore.ml1
-rw-r--r--src/InterpreterExpansion.ml3
-rw-r--r--src/InterpreterProjectors.ml7
-rw-r--r--src/InterpreterUtils.ml4
-rw-r--r--src/Synthesis.ml2
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 = ()