From 9278004b80cf96a1acf9f7d8130d6ced4eabdac8 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 12 May 2026 16:52:31 +0300 Subject: [PATCH 1/3] Extend 74-invalid_deref/36-one-past-pointer with various cases --- .../74-invalid_deref/36-one-past-pointer.c | 25 +++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) 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..7ddbb2d7e3 100644 --- a/tests/regression/74-invalid_deref/36-one-past-pointer.c +++ b/tests/regression/74-invalid_deref/36-one-past-pointer.c @@ -5,8 +5,29 @@ int main(void) { char *buf = malloc(4); 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); // TODO WARN! (unsound) + printf("%p", (void *) end); // TODO WARN (imprecise due to %p) + printf("%s", end + 1); // TODO WARN! (unsound) + printf("%p", (void *) (end + 1)); // TODO WARN (imprecise due to %p) + printf("%s", end - 1); // NOWARN + printf("%p", (void *) (end - 1)); // NOWARN + + 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; } From 474efb67b6f9c46070b2eb97383c1a86b0666ee4 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 12 May 2026 16:58:42 +0300 Subject: [PATCH 2/3] Remove incorrect one-past-end distinction in memOutOfBounds The memOutOfBounds analysis warns about invalid dereferences. Dereferencing one past end is never valid. --- src/analyses/memOutOfBounds.ml | 15 ++++----------- .../74-invalid_deref/36-one-past-pointer.c | 12 ++++++------ 2 files changed, 10 insertions(+), 17 deletions(-) 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 7ddbb2d7e3..7712d325e9 100644 --- a/tests/regression/74-invalid_deref/36-one-past-pointer.c +++ b/tests/regression/74-invalid_deref/36-one-past-pointer.c @@ -13,12 +13,12 @@ int main(void) { printf("%p", (void *) (end + 1)); // TODO WARN (imprecise due to %p) end = buf + 4; // NOWARN - printf("%s", end); // TODO WARN! (unsound) - printf("%p", (void *) end); // TODO WARN (imprecise due to %p) - printf("%s", end + 1); // TODO WARN! (unsound) - printf("%p", (void *) (end + 1)); // TODO WARN (imprecise due to %p) - printf("%s", end - 1); // NOWARN - printf("%p", (void *) (end - 1)); // 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! From 9625835ca18320537ed29f6e949eb2203081df30 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 13 May 2026 10:07:27 +0300 Subject: [PATCH 3/3] Add memory initialization to 74-invalid_deref/36-one-past-pointer --- tests/regression/74-invalid_deref/36-one-past-pointer.c | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) 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 7712d325e9..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,9 +1,15 @@ -// 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 + 3; // NOWARN