summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-06 11:01:44 +0100
committerSon Ho2022-01-06 11:01:44 +0100
commit6a3faa82e09e3fbf23014b53a2b40d420bc70c9b (patch)
tree97cb2ba076c8229a76d168b5ec2ce8e6a87b906f
parent8cac3c5cb5f9c36ffa878cf32ce858d171e4e3c8 (diff)
Cleanup a bit more the dependencies and activate more warnings/errors
-rw-r--r--src/InterpreterBorrows.ml4
-rw-r--r--src/InterpreterExpansion.ml1
-rw-r--r--src/InterpreterPaths.ml1
-rw-r--r--src/InterpreterProjectors.ml5
-rw-r--r--src/dune4
5 files changed, 3 insertions, 12 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 33501939..b60f0973 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -1,12 +1,8 @@
module T = Types
module V = Values
-module E = Expressions
module C = Contexts
module Subst = Substitute
-module A = CfimAst
module L = Logging
-module Inv = Invariants
-module S = Synthesis
open Utils
open InterpreterUtils
open InterpreterProjectors
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 30be657f..46398c84 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -8,7 +8,6 @@ module V = Values
module E = Expressions
module C = Contexts
module Subst = Substitute
-module A = CfimAst
module L = Logging
open TypesUtils
open ValuesUtils
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index fa9fe1a8..e8f5eefc 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -4,7 +4,6 @@ module E = Expressions
module C = Contexts
module Subst = Substitute
module L = Logging
-module Inv = Invariants
module S = Synthesis
open InterpreterUtils
open InterpreterBorrows
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml
index 9a487c89..c3fd0708 100644
--- a/src/InterpreterProjectors.ml
+++ b/src/InterpreterProjectors.ml
@@ -3,12 +3,9 @@ module V = Values
module E = Expressions
module C = Contexts
module Subst = Substitute
-module A = CfimAst
module L = Logging
open TypesUtils
open ValuesUtils
-module Inv = Invariants
-module S = Synthesis
open Utils
open InterpreterUtils
@@ -24,7 +21,7 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
V.abstract_shared_borrows =
(* Sanity check - TODO: move this elsewhere (here we perform the check at every
* recursive call which is a bit overkill...) *)
- let ety = Substitute.erase_regions ty in
+ let ety = Subst.erase_regions ty in
assert (ety = v.V.ty);
(* Project *)
match (v.V.value, ty) with
diff --git a/src/dune b/src/dune
index eab08028..151b2f70 100644
--- a/src/dune
+++ b/src/dune
@@ -9,12 +9,12 @@
-safe-string
-g
;-dsource
- -warn-error -9-11-33-20-21-26-27-39
+ -warn-error -5-8-9-11-14-33-20-21-26-27-39
))
(release (flags
:standard
-safe-string
-g
;-dsource
- -warn-error -9-11-33-20-21-26-27-39
+ -warn-error -5-8-9-11-14-33-20-21-26-27-39
)))