Remove incorrect one-past-end distinction in memOutOfBounds

src/analyses/memOutOfBounds.ml

@@ -38,20 +38,13 @@ struct
     try ID.lt offs (intdom_of_int 0)
     with IntDomain.ArithmeticOnIntegerBot _ -> None
 
-  let check_deref_offset_bounds ptr_size offs =
+  let check_offset_bounds ptr_size offs =
     let ptr_size_le_offs =
       try ID.le ptr_size offs
       with IntDomain.ArithmeticOnIntegerBot _ -> None
     in
     offs_lt_zero offs, ptr_size_le_offs
 
-  let check_ptr_offset_bounds ptr_size offs =
-    let ptr_size_lt_offs =
-      try ID.lt ptr_size offs
-      with IntDomain.ArithmeticOnIntegerBot _ -> None
-    in
-    offs_lt_zero offs, ptr_size_lt_offs
-
   let rec exp_contains_a_ptr (exp:exp) =
     match exp with
     | Const _
@@ -310,7 +303,7 @@ struct
             let casted_offs = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) offs_intdom in (* TODO: proper castkind *)
             let behavior = Undefined MemoryOutOfBoundsAccess in
             let cwe_number = 823 in
-            begin match check_deref_offset_bounds casted_es casted_offs with
+            begin match check_offset_bounds casted_es casted_offs with
               | Some true, _
               | _, Some true ->
                 (set_mem_safety_flag InvalidDeref;
@@ -355,7 +348,7 @@ struct
         | `Lifted ps, ao ->
           let casted_ps = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) ps in (* TODO: proper castkind *)
           let casted_ao = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) ao in (* TODO: proper castkind *)
-          begin match check_ptr_offset_bounds casted_ps casted_ao with
+          begin match check_offset_bounds casted_ps casted_ao with
             | Some true, _
             | _, Some true ->
               set_mem_safety_flag InvalidDeref;
@@ -443,7 +436,7 @@ struct
             | `Lifted ps, `Lifted o ->
               let casted_ps = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) ps in (* TODO: proper castkind *)
               let casted_o = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) o in (* TODO: proper castkind *)
-              begin match check_ptr_offset_bounds casted_ps casted_o with
+              begin match check_offset_bounds casted_ps casted_o with
                 | Some true, _
                 | _, Some true ->
                   set_mem_safety_flag InvalidDeref;

tests/regression/74-invalid_deref/36-one-past-pointer.c

@@ -1,12 +1,39 @@
-// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] memOutOfBounds --enable ana.int.interval
 #include <stdlib.h>
 #include <stdio.h>
 
+extern char __VERIFIER_nondet_char();
+
 int main(void) {
   char *buf = malloc(4);
+  buf[0] = __VERIFIER_nondet_char();
+  buf[1] = __VERIFIER_nondet_char();
+  buf[2] = __VERIFIER_nondet_char();
+  buf[3] = '\0';
   char *end;
-  end = buf + 4; //NOWARN
-  printf("%p", (void *) end); //NOWARN
+
+  end = buf + 3; // NOWARN
+  printf("%s", end); // NOWARN
+  printf("%p", (void *) end); // NOWARN
+  printf("%s", end + 1); // TODO WARN! (unsound)
+  printf("%p", (void *) (end + 1)); // TODO WARN (imprecise due to %p)
+
+  end = buf + 4; // NOWARN
+  printf("%s", end); // WARN!
+  printf("%p", (void *) end); // WARN (imprecise due to %p)
+  printf("%s", end + 1); // WARN! (unsound)
+  printf("%p", (void *) (end + 1)); // WARN (imprecise due to %p)
+  printf("%s", end - 1); // TODO NOWARN (imprecise)
+  printf("%p", (void *) (end - 1)); // TODO NOWARN (imprecise)
+
+  end = buf + 5; // NOWARN
+  printf("%s", end); // WARN!
+  printf("%p", (void *) end); // WARN (imprecise due to %p)
+  printf("%s", end + 1); // WARN!
+  printf("%p", (void *) (end + 1)); // WARN (imprecise due to %p)
+  printf("%s", end - 1); // WARN!
+  printf("%p", (void *) (end - 1)); // WARN (imprecise due to %p)
+
   free(buf);
   return 0;
 }