ExprEngine: sizeof()

This commit is contained in:
Daniel Marjamäki 2020-01-15 15:23:58 +01:00
parent 86d0f62d36
commit c79ec9e956
2 changed files with 17 additions and 0 deletions

View File

@ -1170,6 +1170,18 @@ static ExprEngine::ValuePtr executeAssign(const Token *tok, Data &data)
static ExprEngine::ValuePtr executeFunctionCall(const Token *tok, Data &data)
{
if (Token::simpleMatch(tok->previous(), "sizeof (")) {
ExprEngine::ValuePtr retVal;
if (tok->hasKnownIntValue()) {
const MathLib::bigint value = tok->getKnownIntValue();
retVal = std::make_shared<ExprEngine::IntRange>(std::to_string(value), value, value);
} else {
retVal = std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), 1, 0x7fffffff);
}
call(data.callbacks, tok, retVal, &data);
return retVal;
}
std::vector<ExprEngine::ValuePtr> argValues;
for (const Token *argtok : getArguments(tok)) {
auto val = executeExpression(argtok, data);

View File

@ -72,6 +72,7 @@ private:
TEST_CASE(functionCall1);
TEST_CASE(functionCall2);
TEST_CASE(functionCall3);
TEST_CASE(functionCall4);
TEST_CASE(int1);
@ -435,6 +436,10 @@ private:
ASSERT_EQUALS("-2147483648:2147483647", getRange("int fgets(int, const char *, void *); void f() { int x = -1; fgets(stdin, \"%d\", &x); x=x; }", "x=x"));
}
void functionCall4() {
ASSERT_EQUALS("1:2147483647", getRange("void f() { sizeof(data); }", "sizeof(data)"));
}
void int1() {
ASSERT_EQUALS("(declare-fun $1 () Int)\n"