Make minor modifications

5 files changed, 16 insertions, 5 deletions

diff --git a/TODO.md b/TODO.md
index 8973018f..d92e9640 100644
--- a/TODO.md
+++ b/TODO.md
@@ -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