nits

rems-project · Jan 14, 2025 · 3ce32f9 · 3ce32f9
1 parent 78837ba
commit 3ce32f9
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 17 deletions.
diff --git a/backend/cn/lib/explain.ml b/backend/cn/lib/explain.ml
@@ -143,25 +143,25 @@ and get_var_constraints
            | Owned (_, _) ->
              (* if the predicate is Owned, its pointer argument should not be null *)
              let neq = IT.ne__ psig.pointer (IT.null_ loc) loc in
-             Yes ([LC.T neq], var_cands)
-            | PName name ->
-              (* search for predicate definition *)
-              (match Sym.Map.find_opt name ctxt.global.resource_predicates with
-               | Some pdef ->
-                 (* TODO: this doesn't account for looking up args of the predicate further up in the graph.
-                    Adding that will require dealing with scoping issues, e.g. if
-                    a candidate or line definition for one of the arguments includes a variable with a
-                    different usage within the predicate *)
-                 (match check_pred name pdef v_cand ctxt with
-                  | Yes cs -> Yes (cs, var_cands)
-                  | No e -> No e
-                  | Unknown e -> Unknown e
-                  | Error e -> Error e)
+             Yes ([ LC.T neq ], var_cands)
+           | PName name ->
+             (* search for predicate definition *)
+             (match Sym.Map.find_opt name ctxt.global.resource_predicates with
+              | Some pdef ->
+                (* TODO: this doesn't account for looking up args of the predicate further up in the graph.
+                   Adding that will require dealing with scoping issues, e.g. if
+                   a candidate or line definition for one of the arguments includes a variable with a
+                   different usage within the predicate *)
+                (match check_pred name pdef v_cand ctxt with
+                 | Yes cs -> Yes (cs, var_cands)
+                 | No e -> No e
+                 | Unknown e -> Unknown e
+                 | Error e -> Error e)
               | None ->
                 Unknown (!^"Could not find definition of predicate" ^^^ Sym.pp name)))
         | Q qsig ->
           let _ = qsig in
-          Unknown (!^"Quantified predicates are out of scope for now.")))
+          Unknown !^"Quantified predicates are out of scope for now."))
 
 
 (** End section: Infrastructure for checking if a countermodel satisfies a predicate **)

diff --git a/backend/cn/lib/logicalArgumentTypes.ml b/backend/cn/lib/logicalArgumentTypes.ml
@@ -365,8 +365,8 @@ let rec get_var_cands (exp : IT.t) (candidate : IT.t)
     map_with_guard_unknown (Sym.equal v v' && Id.equal id id') [ exp1 ] [ exp1' ]
   | ArrayShift { base; ct; index }, ArrayShift { base = base'; ct = ct'; index = index' }
     ->
-    map_with_guard_unknown (Sctypes.equal ct ct') [base; index ] [base'; index' ]
-  | CopyAllocId { addr = exp1; loc = exp2 }, CopyAllocId { addr = exp1'; loc=exp2' } ->
+    map_with_guard_unknown (Sctypes.equal ct ct') [ base; index ] [ base'; index' ]
+  | CopyAllocId { addr = exp1; loc = exp2 }, CopyAllocId { addr = exp1'; loc = exp2' } ->
     map_from_IT_lists [ exp1; exp2 ] [ exp1'; exp2' ]
   | HasAllocId exp1, HasAllocId exp1' -> get_var_cands exp1 exp1'
   | SizeOf cty, SizeOf cty' -> map_with_guard_unknown (Sctypes.equal cty cty') [] []