diff options
Diffstat (limited to '')
-rw-r--r-- | src/InterpreterBorrows.ml | 4 | ||||
-rw-r--r-- | src/InterpreterExpansion.ml | 1 | ||||
-rw-r--r-- | src/InterpreterPaths.ml | 1 | ||||
-rw-r--r-- | src/InterpreterProjectors.ml | 5 | ||||
-rw-r--r-- | src/dune | 4 |
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 @@ -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 ))) |