pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[inferbo] Add tests for conditional proof obligations

Browse Source 
Reviewed By: mbouaziz

Differential Revision: D13414441

fbshipit-source-id: bc46414bc
master
Sungkeun Cho 6 years ago committed by Facebook Github Bot
parent 88850d5119
commit f409450d8b
2 changed files with 133 additions and 0 deletions
Show Stats Download Patch File Download Diff File

123
infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp
Unescape View File

@ -0,0 +1,123 @@
/*
* Copyright (c) 2018-present, Facebook, Inc.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
#include <stddef.h>
void conditional_buffer_access(int* ptr, unsigned int size) {
int i;
if (size < 1) {
} else if (size < 2) {
i = *(ptr++);
} else if (size < 3) {
i = *(ptr++);
i = *(ptr++);
} else if (size < 4) {
i = *(ptr++);
i = *(ptr++);
i = *(ptr++);
} else if (size < 5) {
i = *(ptr++);
i = *(ptr++);
i = *(ptr++);
i = *(ptr++);
}
}
void call_conditional_buffer_access_Good_FP() {
int a[1];
conditional_buffer_access(a, 1);
}
void call_conditional_buffer_access_Bad() {
int a[1];
conditional_buffer_access(a, 3);
}
void conditional_buffer_access2(unsigned int n) {
int a[n];
conditional_buffer_access(a, n);
}
void call_conditional_buffer_access2_1_Good_FP() {
conditional_buffer_access2(1);
}
void call_conditional_buffer_access2_2_Good_FP() {
conditional_buffer_access2(3);
}
void conditional_minus(int* ptr, unsigned int size) {
int i = 0;
if (ptr != NULL && (i < size - 1)) {
}
}
void call_conditional_minus_1_Good_FP() { conditional_minus(NULL, 0); }
void call_conditional_minus_2_Good() {
int a[3];
conditional_minus(a, 3);
}
void call_conditional_minus_2_Bad() {
int a[3];
conditional_minus(a, 0);
}
unsigned int conditional_minus2(int* ptr, unsigned int size) {
if (ptr != NULL) {
return (size - 1);
}
}
void call_conditional_minus2_1_Good_FP() { conditional_minus2(NULL, 0); }
void call_conditional_minus2_2_Good() {
int a[3];
conditional_minus2(a, 3);
}
void call_conditional_minus2_2_Bad() {
int a[3];
conditional_minus2(a, 0);
}
enum E {
E_SIZEONE = 0,
E_SIZETWO = 1,
};
void conditional_buffer_access3(int* ptr, int size) {
int i;
switch (ptr[0]) {
case E_SIZETWO:
i = ptr[size - 2];
i = ptr[size - 1];
break;
case E_SIZEONE:
i = ptr[size - 1];
break;
}
}
void call_conditional_buffer_access3_1_Good() {
int a[2];
a[0] = E_SIZETWO;
conditional_buffer_access3(a, 2);
}
void call_conditional_buffer_access3_2_Good_FP() {
int a[1];
a[0] = E_SIZEONE;
conditional_buffer_access3(a, 1);
}
void call_conditional_buffer_access3_Bad() {
int a[1];
a[0] = E_SIZETWO;
conditional_buffer_access3(a, 1);
}

10
infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
Unescape View File

@ -28,6 +28,16 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload1_Bad, 3, BUFFE
codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload2_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Call,Array access: Offset: 5 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 32 Size: 30]
codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access2_1_Good_FP, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter `n`,Array declaration,Call,<Length trace>,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 1 by call to `conditional_buffer_access2` ]
codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access2_2_Good_FP, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter `n`,Array declaration,Call,<Length trace>,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 3 by call to `conditional_buffer_access2` ]
codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access3_2_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `size`,<Length trace>,Parameter `*ptr`,Array access: Offset: -1 Size: 1 by call to `conditional_buffer_access3` ]
codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access3_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `size`,<Length trace>,Parameter `*ptr`,Array access: Offset: -1 Size: 1 by call to `conditional_buffer_access3` ]
codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 1 by call to `conditional_buffer_access` ]
codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access_Good_FP, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 1 by call to `conditional_buffer_access` ]
codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus2_1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus2` ]
codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus2_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus2` ]
codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus_1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus` ]
codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus` ]
codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,<Length trace>,Parameter `*__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter `__n`,Assignment,Call,Parameter `__x->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Assignment,Binary operation: (1 - [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: lib,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]

Write Preview
Loading…
Cancel
Save