Update condition for non-zero return by strncmp

goblint · Jul 20, 2023 · 780e02a · 780e02a
1 parent 9d21da4
commit 780e02a
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/src/cdomains/arrayDomain.ml b/src/cdomains/arrayDomain.ml
@@ -1687,8 +1687,9 @@ struct
         Idx.starting IInt Z.one
       else 
         (* if first null bytes are certain, have different indexes and are before index n if n present, return integer <> 0 *)
-        (try if Z.equal (must_nulls_min_elt must_nulls_set1) (may_nulls_min_elt may_nulls_set1) && (not n_exists || Z.lt (must_nulls_min_elt must_nulls_set1) n)
-                && Z.equal (must_nulls_min_elt must_nulls_set2) (may_nulls_min_elt may_nulls_set2) && (not n_exists || Z.lt (must_nulls_min_elt must_nulls_set2) n)
+        (try if Z.equal (must_nulls_min_elt must_nulls_set1) (may_nulls_min_elt may_nulls_set1) 
+                && Z.equal (must_nulls_min_elt must_nulls_set2) (may_nulls_min_elt may_nulls_set2)
+                && (not n_exists || Z.lt (must_nulls_min_elt must_nulls_set1) n || Z.lt (must_nulls_min_elt must_nulls_set2) n )
                 && not (Z.equal (must_nulls_min_elt must_nulls_set1) (must_nulls_min_elt must_nulls_set2)) then
              Idx.of_excl_list IInt [Z.zero]
            else