Skip to content

Commit 8748522

Browse files
authored
Merge pull request #1932 from goblint/calloc-speculating
Fix spurious `*` overflow check in `calloc` implementation
2 parents f857a3a + 7e1ecf6 commit 8748522

File tree

2 files changed

+13
-1
lines changed

2 files changed

+13
-1
lines changed

src/analyses/base.ml

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2763,7 +2763,11 @@ struct
27632763
let blob_set = Option.map_default (fun heap_var -> [heap_var, TVoid [], VD.Blob (VD.bot (), sizeval, ZeroInit.calloc)]) [] heap_var in
27642764
set_many ~man st ((eval_lv ~man st lv, (Cilfacade.typeOfLval lv), Address addr):: blob_set)
27652765
else
2766-
let blobsize = ID.mul (ID.cast_to ~kind:Internal ik @@ sizeval) (ID.cast_to ~kind:Internal ik @@ countval) in (* TODO: proper castkind *)
2766+
let blobsize = (* only speculative during ID.mul *)
2767+
(* TODO: Since C23, calloc returns NULL when this multiplication would overflow, but int domains don't return overflow information here currently; needs refactor to not produce overflow warnings inside domains *)
2768+
let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in
2769+
ID.mul (ID.cast_to ~kind:Internal ik @@ sizeval) (ID.cast_to ~kind:Internal ik @@ countval) (* TODO: proper castkind *)
2770+
in
27672771
let offset = `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero, `NoOffset) in
27682772
(* the heap_var is the base address of the allocated memory, but we need to keep track of the offset for the blob *)
27692773
let addr_offset = AD.map (fun a -> Addr.add_offset a offset) addr in
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
// PARAM: --enable ana.int.interval
2+
#include <stdlib.h>
3+
4+
int main() {
5+
size_t a, b;
6+
unsigned char *randomString = (unsigned char *)calloc(a,b); // NOWARN (signed integer overflow in *)
7+
return 0;
8+
}

0 commit comments

Comments
 (0)