diff options
| -rw-r--r-- | TODO.md | 2 | ||||
| -rw-r--r-- | src/CfimAst.ml | 4 | ||||
| -rw-r--r-- | src/Expressions.ml | 4 | ||||
| -rw-r--r-- | src/SymbolicAst.ml | 1 | ||||
| -rw-r--r-- | src/SymbolicAstUtils.ml | 10 |
5 files changed, 16 insertions, 5 deletions
@@ -1,5 +1,7 @@ # TODO +0. update the end borrows internal to abstractions to not introduce a Bottom + 1. stateful maps/sets modules (hashtbl?) 1. Check the occurrence of visitors like visit_AEndedMutLoan: the parameters are diff --git a/src/CfimAst.ml b/src/CfimAst.ml index 6d8c03e4..57122a51 100644 --- a/src/CfimAst.ml +++ b/src/CfimAst.ml @@ -17,10 +17,10 @@ type var = { (** A variable, as used in a function definition *) type assumed_fun_id = BoxNew | BoxDeref | BoxDerefMut | BoxFree -[@@deriving show] +[@@deriving show, ord] type fun_id = Local of FunDefId.id | Assumed of assumed_fun_id -[@@deriving show] +[@@deriving show, ord] type assertion = { cond : operand; expected : bool } [@@deriving show] diff --git a/src/Expressions.ml b/src/Expressions.ml index 6a7e92a0..76733941 100644 --- a/src/Expressions.ml +++ b/src/Expressions.ml @@ -19,7 +19,7 @@ type place = { var_id : VarId.id; projection : projection } [@@deriving show] type borrow_kind = Shared | Mut | TwoPhaseMut [@@deriving show] -type unop = Not | Neg [@@deriving show] +type unop = Not | Neg [@@deriving show, ord] (** A binary operation @@ -45,7 +45,7 @@ type binop = | Mul | Shl | Shr -[@@deriving show] +[@@deriving show, ord] (** Constant value for an operand diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml index 00431ebd..fc2b2fc4 100644 --- a/src/SymbolicAst.ml +++ b/src/SymbolicAst.ml @@ -14,6 +14,7 @@ type call_id = (** A "regular" function (i.e., a function which is not a primitive operation) *) | Unop of E.unop | Binop of E.binop +[@@deriving show, ord] type call = { call_id : call_id; diff --git a/src/SymbolicAstUtils.ml b/src/SymbolicAstUtils.ml index 7b93b019..f781ed65 100644 --- a/src/SymbolicAstUtils.ml +++ b/src/SymbolicAstUtils.ml @@ -55,7 +55,15 @@ let get_top_owned_ended_loans_borrows (abs : V.abs) : ended_loan_or_borrow list | AEndedMutLoan { child = _; given_back = _; given_back_meta } -> (* Add the meta-value and stop the exploration *) add_cloan given_back_meta - | AEndedSharedLoan (_, _) -> raise Unimplemented + | 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 |