Skip to content

Commit 6b1f72b

Browse files
authored
Merge pull request #1761 from Robotechnic/master
Fix for #1758
2 parents ff6f52c + d64a5a3 commit 6b1f72b

File tree

3 files changed

+13
-1
lines changed

3 files changed

+13
-1
lines changed

src/analyses/base.ml

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2492,7 +2492,9 @@ struct
24922492
| _ ->
24932493
set ~man st lv_a lv_typ (VD.top_value (unrollType lv_typ))
24942494
end
2495-
in
2495+
in
2496+
(* Evaluate each functions arguments. `eval_rv` is only called for its side effects, we ignore the result. *)
2497+
List.iter (fun arg -> eval_rv ~man st arg |> ignore) args;
24962498
let st = match desc.special args, f.vname with
24972499
| Memset { dest; ch; count; }, _ ->
24982500
(* TODO: check count *)

tests/regression/26-undefined_behavior/02-array-out-of-bounds.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ int main()
1111
for (int i = 0; i < 10; ++i)
1212
{
1313
arr[i] = 5; //WARN
14+
printf("%d\n", arr[i]); //WARN
1415
}
1516
return 0;
1617
}
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
//PARAM: --enable ana.int.interval
2+
3+
#include <limits.h>
4+
#include <stdio.h>
5+
6+
int main() {
7+
printf("%d\n", INT_MAX + 1); //WARN
8+
return 0;
9+
}

0 commit comments

Comments
 (0)