http://cppcheck1.osuosl.org:8000/z3" rel="nofollow">http://cppcheck1.osuosl.org:8000/z3 ``` 2019-09-22 03:00 ftp://ftp.se.debian.org/debian/pool/main/z/z3/z3_4.8.4.orig.tar.gz cppcheck-options: -j1 --library=posix --library=gnu --library=openmp -D__GNUC__ --check-library --inconclusive --enable=style,information --platform=unix64 --template=daca2 -rp=temp temp platform: Linux-4.15.0-64-generic-x86_64-with-Ubuntu-18.04-bionic python: 2.7.15+ client-version: 1.1.37 cppcheck: head 1.89 head-info: 6c9839a (2019-09-21 21:42:13 +0200) count: Crash! Crash! elapsed-time: -11.0 -11.0 head results: Checking temp/z3-z3-4.8.4/src/nlsat/nlsat_explain.cpp: __GNUC__=1... Program received signal SIGSEGV, Segmentation fault. singleMemberCallInScope (start=start@entry=0x555555e76750, varid=397, input=@0x7fffffffb25e: false) at build/checkstl.cpp:3976 3976 if (isVariableChanged(dotTok->next(), endStatement, dotTok->astOperand1()->varId(), false, nullptr, true)) #0 singleMemberCallInScope (start=start@entry=0x555555e76750, varid=397, input=@0x7fffffffb25e: false) at build/checkstl.cpp:3976 #1 0x000055555566d0c5 in CheckStl::useStlAlgorithm (this=this@entry=0x7fffffffb390) at build/checkstl.cpp:4144 cppcheck-opensource#2 0x000055555567d6ed in CheckStl::runChecks (this=<optimized out>, tokenizer=<optimized out>, settings=0x7fffffffcd50, errorLogger=0x7fffffffcb30) at lib/checkstl.h:74 cppcheck-opensource#3 0x00005555556a9150 in CppCheck::checkNormalTokens (this=this@entry=0x7fffffffcb30, tokenizer=...) at build/cppcheck.cpp:732 cppcheck-opensource#4 0x00005555556adb6e in CppCheck::checkFile (this=this@entry=0x7fffffffcb30, filename="temp/z3-z3-4.8.4/src/nlsat/nlsat_explain.cpp", cfgname="", fileStream=...) at build/cppcheck.cpp:542 cppcheck-opensource#5 0x00005555556b18bc in CppCheck::check (this=this@entry=0x7fffffffcb30, path="temp/z3-z3-4.8.4/src/nlsat/nlsat_explain.cpp") at build/cppcheck.cpp:197 cppcheck-opensource#6 0x0000555555809337 in CppCheckExecutor::check_internal (this=this@entry=0x7fffffffd8c0, cppcheck=..., argv=argv@entry=0x7fffffffdc48) at cli/cppcheckexecutor.cpp:884 cppcheck-opensource#7 0x0000555555809c6a in CppCheckExecutor::check (this=0x7fffffffd8c0, argc=14, argv=0x7fffffffdc48) at cli/cppcheckexecutor.cpp:198 cppcheck-opensource#8 0x00005555555b899b in main (argc=14, argv=0x7fffffffdc48) at cli/main.cpp:95 ``` Due to code like the following, when cppcheck does not have the macros `DEBUG_CODE` or `TRACE` defined: ``` DEBUG_CODE( TRACE("nlsat", for (literal l : result) { m_solver.display(tout << " ", l); } tout << "\n"; ); for (literal l : result) { CTRACE("nlsat", l_true != m_solver.value(l), m_solver.display(tout, l) << " " << m_solver.value(l) << "\n";); SASSERT(l_true == m_solver.value(l)); }); ```

Commits

Commits on Oct 8, 2019

Fix crashes in z3