diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 4546fda32e..7461f79382 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/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; diff --git a/tests/regression/74-invalid_deref/36-one-past-pointer.c b/tests/regression/74-invalid_deref/36-one-past-pointer.c index b4ceb506d7..e3744a027b 100644 --- a/tests/regression/74-invalid_deref/36-one-past-pointer.c +++ b/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 #include +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; }