diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/PrintSymbolicAst.ml | 1 | ||||
| -rw-r--r-- | src/SymbolicAstUtils.ml | 94 | ||||
| -rw-r--r-- | src/main.ml | 1 |
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 |