walkero
/
cppcheck
1
0
Fork 0
Code Issues Pull Requests Projects Releases 1 Wiki Activity

Verification; Juliet *_float_* division by zero tests

This commit is contained in:
Daniel Marjamäki 2019-12-31 09:01:58 +01:00
parent 82c91f9484
commit 3af3219076
2 changed files with 10 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
lib/exprengine.cpp
View File

@ -788,6 +788,10 @@ bool ExprEngine::FloatRange::isEqual(DataBase *dataBase, int value) const
const Data *data = dynamic_cast<Data *>(dataBase); const Data *data = dynamic_cast<Data *>(dataBase);
if (data->constraints.empty()) if (data->constraints.empty())
return true; return true;
if (MathLib::isFloat(name)) {
float f = MathLib::toDoubleNumber(name);
return value >= f - 0.00001 && value <= f + 0.00001;
}
#ifdef USE_Z3 #ifdef USE_Z3
// Check the value against the constraints // Check the value against the constraints
ExprData exprData; ExprData exprData;
@ -797,7 +801,7 @@ bool ExprEngine::FloatRange::isEqual(DataBase *dataBase, int value) const
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints) for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint)); solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver); exprData.addAssertions(solver);
solver.add(e == value); solver.add(e >= value && e <= value);
return solver.check() != z3::unsat; return solver.check() != z3::unsat;
} catch (const z3::exception &exception) { } catch (const z3::exception &exception) {
std::cerr << "z3: " << exception << std::endl; std::cerr << "z3: " << exception << std::endl;
@ -817,6 +821,8 @@ bool ExprEngine::FloatRange::isGreaterThan(DataBase *dataBase, int value) const
const Data *data = dynamic_cast<Data *>(dataBase); const Data *data = dynamic_cast<Data *>(dataBase);
if (data->constraints.empty()) if (data->constraints.empty())
return true; return true;
if (MathLib::isFloat(name))
return value > MathLib::toDoubleNumber(name);
#ifdef USE_Z3 #ifdef USE_Z3
// Check the value against the constraints // Check the value against the constraints
ExprData exprData; ExprData exprData;
@ -846,6 +852,8 @@ bool ExprEngine::FloatRange::isLessThan(DataBase *dataBase, int value) const
const Data *data = dynamic_cast<Data *>(dataBase); const Data *data = dynamic_cast<Data *>(dataBase);
if (data->constraints.empty()) if (data->constraints.empty())
return true; return true;
if (MathLib::isFloat(name))
return value < MathLib::toDoubleNumber(name);
#ifdef USE_Z3 #ifdef USE_Z3
// Check the value against the constraints // Check the value against the constraints
ExprData exprData; ExprData exprData;

3
test/verify/juliet.py
View File

@ -61,8 +61,7 @@ def check(tc:str, warning_id:str):
final_report = '' final_report = ''
final_report += check('C/testcases/CWE369_Divide_by_Zero/s*/*_int_*.c', 'verificationDivByZero') final_report += check('C/testcases/CWE369_Divide_by_Zero/s*/*.c', 'verificationDivByZero')
#final_report += check('C/testcases/CWE476_*/*.c', 'verificationNullPointerDereference')
print(final_report) print(final_report)