Integrate review suggestions

goblint · Oct 9, 2023 · 5ac2f23 · 5ac2f23
1 parent 48d0e5d
commit 5ac2f23
Show file tree

Hide file tree

Showing 4 changed files with 274 additions and 318 deletions.
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -2047,7 +2047,7 @@ struct
     in
     let address_from_value (v:value) = match v with
       | Address a ->
-        let rec lo:'a Offset_intf.t -> 'a Offset_intf.t = function
+        let rec lo = function
           | `Index (i, `NoOffset) -> `NoOffset
           | `NoOffset -> `NoOffset
           | `Field (f, o) -> `Field (f, lo o)
@@ -2191,9 +2191,9 @@ struct
              if it surely isn't, assign a null_ptr *)
           string_manipulation haystack needle lv true (Some (fun h_a n_a -> Address (AD.substring_extraction h_a n_a)))
               (fun h_ar n_ar -> match CArrays.substring_extraction h_ar n_ar with
-                | true, false -> Address (AD.null_ptr)
-                | false, true -> Address (eval_lv (Analyses.ask_of_ctx ctx) gs st (mkMem ~addr:(Cil.stripCasts haystack) ~off:NoOffset))
-                | _ -> Address (AD.join (eval_lv (Analyses.ask_of_ctx ctx) gs st
+                | CArrays.IsNotSubstr -> Address (AD.null_ptr)
+                | CArrays.IsSubstrAtIndex0 -> Address (eval_lv (Analyses.ask_of_ctx ctx) gs st (mkMem ~addr:(Cil.stripCasts haystack) ~off:NoOffset))
+                | CArrays.IsMaybeSubstr -> Address (AD.join (eval_lv (Analyses.ask_of_ctx ctx) gs st
                                            (mkMem ~addr:(Cil.stripCasts haystack) ~off:(Index (Offset.Index.Exp.any, NoOffset)))) (AD.null_ptr)))
         | None -> st
       end