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

Remove NEW_Z3 macro

This commit is contained in:
Daniel Marjamäki 2020-05-12 16:57:07 +02:00
parent dab0180aef
commit 3e650c311b
3 changed files with 19 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.travis.yml
View File

@ -63,6 +63,7 @@ matrix:
compiler: gcc compiler: gcc
script: script:
- make clean - make clean
- cp externals/z3_version_old.h externals/z3_version.h
- make USE_Z3=yes -j2 all - make USE_Z3=yes -j2 all
- ./testrunner TestExprEngine - ./testrunner TestExprEngine
- python3 test/bug-hunting/cve.py - python3 test/bug-hunting/cve.py

12
externals/z3_version_old.h vendored Normal file
View File

@ -0,0 +1,12 @@
#ifndef Z3_MAJOR_VERSION
#define Z3_MAJOR_VERSION 0
#endif
#ifndef Z3_MINOR_VERSION
#define Z3_MINOR_VERSION 0
#endif
#ifndef Z3_BUILD_NUMBER
#define Z3_BUILD_NUMBER 0
#endif

9
lib/exprengine.cpp
View File

@ -142,6 +142,9 @@
#include <iostream> #include <iostream>
#ifdef USE_Z3 #ifdef USE_Z3
#include <z3++.h> #include <z3++.h>
#include <z3_version.h>
#define GET_VERSION_INT(A,B,C) ((A) * 10000 + (B) * 100 + (C))
#define Z3_VERSION_INT GET_VERSION_INT(Z3_MAJOR_VERSION, Z3_MINOR_VERSION, Z3_BUILD_NUMBER)
#endif #endif
namespace { namespace {
@ -782,7 +785,7 @@ struct ExprData {
} }
z3::expr addFloat(const std::string &name) { z3::expr addFloat(const std::string &name) {
#ifdef NEW_Z3 #if Z3_VERSION_INT >= GET_VERSION_INT(4,8,0)
z3::expr e = context.fpa_const(name.c_str(), 11, 53); z3::expr e = context.fpa_const(name.c_str(), 11, 53);
#else #else
z3::expr e = context.real_const(name.c_str()); z3::expr e = context.real_const(name.c_str());
@ -804,7 +807,7 @@ struct ExprData {
if (b->binop == "/") if (b->binop == "/")
return op1 / op2; return op1 / op2;
if (b->binop == "%") if (b->binop == "%")
#ifdef NEW_Z3 #if Z3_VERSION_INT >= GET_VERSION_INT(4,8,0)
return op1 % op2; return op1 % op2;
#else #else
return op1 - (op1 / op2) * op2; return op1 - (op1 / op2) * op2;
@ -837,7 +840,7 @@ struct ExprData {
throw VerifyException(nullptr, "Can not solve expressions, operand value is null"); throw VerifyException(nullptr, "Can not solve expressions, operand value is null");
if (auto intRange = std::dynamic_pointer_cast<ExprEngine::IntRange>(v)) { if (auto intRange = std::dynamic_pointer_cast<ExprEngine::IntRange>(v)) {
if (intRange->name[0] != '$') if (intRange->name[0] != '$')
#ifdef NEW_Z3 #if Z3_VERSION_INT >= GET_VERSION_INT(4,8,0)
return context.int_val(int64_t(intRange->minValue)); return context.int_val(int64_t(intRange->minValue));
#else #else
return context.int_val((long long)(intRange->minValue)); return context.int_val((long long)(intRange->minValue));