diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 63ba481ba..be4d75cac 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -136,6 +136,14 @@ let memcpy dest_exp src_exp size_exp = {exec; check} +let memset arr_exp size_exp = + let exec _ ~ret:_ mem = mem + and check {location} mem cond_set = + BoUtils.Check.lindex_byte ~array_exp:arr_exp ~byte_index_exp:size_exp mem location cond_set + in + {exec; check} + + let realloc src_exp size_exp = let exec {location; tenv} ~ret:(id, _) mem = let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in @@ -477,6 +485,7 @@ module Call = struct ; -"strlen" <>--> by_value Dom.Val.Itv.nat ; -"memcpy" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> memcpy ; -"memmove" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> memcpy + ; -"memset" <>$ capt_exp $+ any_arg $+ capt_exp $!--> memset ; -"boost" &:: "split" $ capt_arg_of_typ (-"std" &:: "vector") $+ any_arg $+ any_arg $+? any_arg $--> Boost.Split.std_vector diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 40bc17c29..99a6ad264 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -74,6 +74,9 @@ codetoanalyze/c/bufferoverrun/models.c, memmove_bad1, 3, BUFFER_OVERRUN_L1, no_b codetoanalyze/c/bufferoverrun/models.c, memmove_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 44 Size: 40] codetoanalyze/c/bufferoverrun/models.c, memmove_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 40] codetoanalyze/c/bufferoverrun/models.c, memmove_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 8 Size: 4] +codetoanalyze/c/bufferoverrun/models.c, memset_bad1, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 44 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, memset_bad2, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, memset_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 8 Size: 4] codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: 10] codetoanalyze/c/bufferoverrun/pointer_arith.c, FP_pointer_arith5_Ok, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [3, 2043] Size: 1024] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/models.c b/infer/tests/codetoanalyze/c/bufferoverrun/models.c index 6a6458344..1333f1874 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/models.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/models.c @@ -145,3 +145,39 @@ void memmove_good4() { int dst[3]; memmove(dst, src, sizeof(dst)); } + +void memset_bad1() { + int arr[10]; + memset(arr, 0, 44); +} + +void memset_bad2() { + int arr[10]; + memset(arr, 0, -1); +} + +void memset_bad3() { + int arr[1]; + int* dst = &arr[0]; + memset(dst, 0, sizeof(dst)); +} + +void memset_good1() { + int arr[10]; + memset(arr, 0, 40); +} + +void memset_good2() { + int arr[10]; + memset(arr, 0, 0); +} + +void memset_good3() { + int arr[10]; + memset(arr, 0, 20); +} + +void memset_good4() { + int arr[10]; + memset(arr, 0, sizeof(arr)); +}