Verification; test

This commit is contained in:
Daniel Marjamäki 2019-12-31 06:08:04 +01:00
parent fde86b696d
commit 7dcfd3400f
2 changed files with 36 additions and 12 deletions

View File

@ -1,3 +1,6 @@
// make USE_Z3=yes
// ./cppcheck --verify --inline-suppr --enable=information test/testsuites/danmar-verify/divbyzero.cpp
struct S { int x; };
@ -10,7 +13,22 @@ void callfunc1() {
return 100000 / x;
}
void g1() {
void float1(float f) {
// cppcheck-suppress verificationDivByZero
return 100000 / (int)f;
}
void float2(float f) {
// cppcheck-suppress verificationDivByZeroFloat
return 100000 / f;
}
void functionCall() {
// cppcheck-suppress verificationDivByZero
return 100000 / unknown_function();
}
void globalVar1() {
// cppcheck-suppress verificationDivByZero
return 100000 / globalvar;
}
@ -25,16 +43,6 @@ void pointer2(int *p) {
return 100000 / p[32];
}
void float1(float f) {
// cppcheck-suppress verificationDivByZero
return 100000 / (int)f;
}
void float2(float f) {
// cppcheck-suppress verificationDivByZeroFloat
return 100000 / f;
}
void stdmap(std::map<int,int> &data) {
// cppcheck-suppress verificationDivByZero
return 100000 / data[43];

View File

@ -1,7 +1,23 @@
int foo() {
// make USE_Z3=yes CPPFLAGS=-DVERIFY_UNININIT
// ./cppcheck --verify --inline-suppr --enable=information test/testsuites/danmar-verify/uninit.c
int array1() {
int a[10];
a[0] = 0;
// cppcheck-suppress verificationUninit
return a[2];
}
int array2() {
int a[10][10];
a[0][0] = 0;
// cppcheck-suppress verificationUninit
return a[2][3];
}
int pointer1(int *p) {
// cppcheck-suppress verificationUninit
return *p;
}