summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-24 07:45:46 +0100
committerSon Ho2022-01-24 07:45:46 +0100
commit3f10869014d639199fc18df661c3faf3b90e6462 (patch)
tree304ac5e3b7e9475496a16d5819abf427483f760f /src
parent67131cfdb02a70a97a6a4654c2eaed96cf958164 (diff)
Make minor modifications
Diffstat (limited to '')
-rw-r--r--src/CfimAst.ml4
-rw-r--r--src/Expressions.ml4
-rw-r--r--src/SymbolicAst.ml1
-rw-r--r--src/SymbolicAstUtils.ml10
4 files changed, 14 insertions, 5 deletions
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