summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/PrintSymbolicAst.ml1
-rw-r--r--src/SymbolicAstUtils.ml94
-rw-r--r--src/main.ml1
3 files changed, 0 insertions, 96 deletions
diff --git a/src/PrintSymbolicAst.ml b/src/PrintSymbolicAst.ml
index ec07a270..25b39e2e 100644
--- a/src/PrintSymbolicAst.ml
+++ b/src/PrintSymbolicAst.ml
@@ -15,7 +15,6 @@ module A = CfimAst
module C = Contexts
module M = Modules
open SymbolicAst
-open SymbolicAstUtils
module P = Print
module PT = Print.Types
diff --git a/src/SymbolicAstUtils.ml b/src/SymbolicAstUtils.ml
deleted file mode 100644
index 0f25e6b8..00000000
--- a/src/SymbolicAstUtils.ml
+++ /dev/null
@@ -1,94 +0,0 @@
-open Errors
-module T = Types
-module V = Values
-module E = Expressions
-module A = CfimAst
-open SymbolicAst
-open ValuesUtils
-open InterpreterUtils
-
-type ('c, 's) ended = EndedConcrete of 'c | EndedSymbolic of 's
-
-type ended_loan = (V.mvalue, V.msymbolic_value list) ended
-
-type ended_borrow = (V.msymbolic_value, V.msymbolic_value) ended
-
-type ended_loan_or_borrow =
- | EndedLoan of ended_loan
- | EndedBorrow of ended_borrow
-
-(** Return the list of the meta-values given to the top owned ended mutable
- loans/borrows of an abstraction
-
- We expect an abstraction where all the loans/borrows have ended.
-
- TODO: remove
- *)
-let get_top_owned_ended_loans_borrows (abs : V.abs) : ended_loan_or_borrow list
- =
- (* The accumulator *)
- let acc = ref [] in
- let add x = acc := x :: !acc in
- let add_loan x = add (EndedLoan x) in
- let add_borrow x = add (EndedBorrow x) in
- let add_sloan x = add_loan (EndedSymbolic x) in
- let add_cloan x = add_loan (EndedConcrete x) in
- let add_sborrow x = add_borrow (EndedSymbolic x) in
- let add_cborrow x = add_borrow (EndedConcrete x) in
-
- (* The visitor *)
- let obj =
- object
- inherit [_] V.iter_abs as super
-
- method! visit_aproj env aproj =
- match aproj with
- | AEndedProjLoans (msv, []) ->
- (* The symbolic value was left unchanged *)
- add_sloan [ msv ]
- | AEndedProjLoans (_, mvl) -> add_sloan (List.map fst mvl)
- | AEndedProjBorrows mv -> add_sborrow mv
- | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) ->
- failwith "Unreachable"
-
- method! visit_aloan_content env lc =
- match lc with
- | AMutLoan (_, _) | ASharedLoan (_, _, _) -> failwith "Unreachable"
- | AEndedMutLoan { child = _; given_back = _; given_back_meta } ->
- (* Add the meta-value and stop the exploration *)
- add_cloan given_back_meta
- | AEndedSharedLoan (_, _) ->
- (* We don't dive into shared loans: there is nothing to give back
- * inside (note that there could be a mutable borrow in the shared
- * value, pointing to a mutable loan in the child avalue, but this
- * borrow is in practice immutable *)
- ()
- | AIgnoredMutLoan (_, _) ->
- (* There can be *inner* mutable loans, but not outer ones *)
- failwith "Unreachable"
- | AEndedIgnoredMutLoan _ ->
- (* Dive in *)
- super#visit_aloan_content env lc
- | AIgnoredSharedLoan _ ->
- (* Ignore *)
- ()
-
- method! visit_aborrow_content env bc =
- match bc with
- | AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
- failwith "Unreachable"
- | AEndedMutBorrow (mv, _) ->
- (* Add the meta-value and stop the exploration *)
- add_cborrow mv
- | AEndedIgnoredMutBorrow _ ->
- (* Dive in *)
- super#visit_aborrow_content env bc
- | AProjSharedBorrow _ ->
- (* Ignore *)
- ()
- end
- in
- (* Apply *)
- obj#visit_abs () abs;
- (* Return the accumulated values *)
- List.rev !acc
diff --git a/src/main.ml b/src/main.ml
index 492470c7..a7480a3f 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -7,7 +7,6 @@ module I = Interpreter
module EL = Easy_logging.Logging
module TA = TypesAnalysis
module P = Pure
-open SymbolicAstUtils
open PrintSymbolicAst
open SymbolicToPure