From 3f10869014d639199fc18df661c3faf3b90e6462 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 24 Jan 2022 07:45:46 +0100
Subject: Make minor modifications

---
 src/CfimAst.ml          |  4 ++--
 src/Expressions.ml      |  4 ++--
 src/SymbolicAst.ml      |  1 +
 src/SymbolicAstUtils.ml | 10 +++++++++-
 4 files changed, 14 insertions(+), 5 deletions(-)

(limited to 'src')

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
-- 
cgit v1.2.3