From 33446d0c75bc351efbacdf5c413e3a9fd2a29e3e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= Date: Mon, 3 Jan 2022 17:10:01 +0100 Subject: [PATCH] exprengine; add CONTRACT #define so contract-handling can be enabled/disabled --- lib/exprengine.cpp | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index f35727771..364a3f5cd 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -151,6 +151,7 @@ #endif constexpr auto MAX_BUFFER_SIZE = ~0UL; +#define CONTRACT 1 namespace { struct ExprEngineException { @@ -412,6 +413,7 @@ namespace { return tokenizer->isCPP(); } +#ifdef CONTRACT ExprEngine::ValuePtr executeContract(const Function *function, ExprEngine::ValuePtr (*executeExpression)(const Token*, Data&)) { const auto it = settings->functionContracts.find(function->fullName()); if (it == settings->functionContracts.end()) @@ -439,6 +441,7 @@ namespace { if (value) constraints.push_back(value); } +#endif void assignValue(const Token *tok, unsigned int varId, ExprEngine::ValuePtr value) { if (varId == 0) @@ -617,6 +620,7 @@ namespace { } void addConstraints(ExprEngine::ValuePtr value, const Token *tok) { +#ifdef CONTRACT MathLib::bigint low; if (tok->getCppcheckAttribute(TokenImpl::CppcheckAttributes::Type::LOW, &low)) addConstraint(std::make_shared(">=", value, std::make_shared(std::to_string(low), low, low)), true); @@ -624,6 +628,7 @@ namespace { MathLib::bigint high; if (tok->getCppcheckAttribute(TokenImpl::CppcheckAttributes::Type::HIGH, &high)) addConstraint(std::make_shared("<=", value, std::make_shared(std::to_string(high), high, high)), true); +#endif } void reportError(const Token *tok, @@ -1968,6 +1973,7 @@ static ExprEngine::ValuePtr executeIncDec(const Token *tok, Data &data) #ifdef USE_Z3 static void checkContract(Data &data, const Token *tok, const Function *function, const std::vector &argValues) { +#ifdef CONTRACT ExprData exprData; z3::solver solver(exprData.context); try { @@ -2037,6 +2043,7 @@ static void checkContract(Data &data, const Token *tok, const Function *function true, functionName); } +#endif } #endif @@ -2096,6 +2103,7 @@ static ExprEngine::ValuePtr executeFunctionCall(const Token *tok, Data &data) if (tok->astOperand1()->function()) { const Function *function = tok->astOperand1()->function(); const std::string &functionName = function->fullName(); +#ifdef CONTRACT const auto contractIt = data.settings->functionContracts.find(functionName); if (contractIt != data.settings->functionContracts.end()) { #ifdef USE_Z3 @@ -2108,6 +2116,7 @@ static ExprEngine::ValuePtr executeFunctionCall(const Token *tok, Data &data) if (!bailout) data.addMissingContract(functionName); } +#endif // Execute subfunction.. if (hasBody) { @@ -2996,7 +3005,9 @@ void ExprEngine::executeFunction(const Scope *functionScope, ErrorLogger *errorL for (const Variable &arg : function->argumentList) data.assignValue(functionScope->bodyStart, arg.declarationId(), createVariableValue(arg, data)); +#ifdef CONTRACT data.contractConstraints(function, executeExpression1); +#endif const std::time_t stopTime = data.startTime + data.settings->bugHuntingCheckFunctionMaxTime;