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

exprengine: reduce max buffer size to int_max

This commit is contained in:
Daniel Marjamäki 2022-01-03 20:55:46 +01:00
parent 0cba2962ba
commit 3524a0a3eb
2 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lib/exprengine.cpp
View File

@ -150,7 +150,7 @@
#define Z3_VERSION_INT GET_VERSION_INT(Z3_MAJOR_VERSION, Z3_MINOR_VERSION, Z3_BUILD_NUMBER) #define Z3_VERSION_INT GET_VERSION_INT(Z3_MAJOR_VERSION, Z3_MINOR_VERSION, Z3_BUILD_NUMBER)
#endif #endif
const std::uint64_t MAX_BUFFER_SIZE = ~0ULL; const uint32_t MAX_BUFFER_SIZE = ~0U >> 1;
#define CONTRACT 1 #define CONTRACT 1
namespace { namespace {

2
test/testexprengine.cpp
View File

@ -814,7 +814,7 @@ private:
" *x = 1;\n" " *x = 1;\n"
"}"; "}";
ASSERT_EQUALS("1:28: $2=ArrayValue([$1],[:]=?,null)\n" ASSERT_EQUALS("1:28: $2=ArrayValue([$1],[:]=?,null)\n"
"1:28: $1=IntRange(1:ffffffffffffffff)\n" "1:28: $1=IntRange(1:2147483647)\n"
"1:28: D0:memory:{x=($2,[$1],[:]=?)}\n" "1:28: D0:memory:{x=($2,[$1],[:]=?)}\n"
"2:9: D0:memory:{x=($2,[$1],[:]=?,[0]=2)}\n" "2:9: D0:memory:{x=($2,[$1],[:]=?,[0]=2)}\n"
"3:9: D0:memory:{x=($2,[$1],[:]=?,[0]=1)}\n", "3:9: D0:memory:{x=($2,[$1],[:]=?,[0]=1)}\n",