From 172cd2db8e312e366f27f4218e48d535c8d3bf5b Mon Sep 17 00:00:00 2001
From: Ken-Patrick Lehrmann <kp.lehrmann@gmail.com>
Date: Sun, 22 Sep 2019 20:50:56 +0200
Subject: [PATCH] Fix crashes in z3

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: 6c9839a58 (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
 #2  0x000055555567d6ed in CheckStl::runChecks (this=<optimized out>, tokenizer=<optimized out>, settings=0x7fffffffcd50, errorLogger=0x7fffffffcb30) at lib/checkstl.h:74
 #3  0x00005555556a9150 in CppCheck::checkNormalTokens (this=this@entry=0x7fffffffcb30, tokenizer=...) at build/cppcheck.cpp:732
 #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
 #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
 #6  0x0000555555809337 in CppCheckExecutor::check_internal (this=this@entry=0x7fffffffd8c0, cppcheck=..., argv=argv@entry=0x7fffffffdc48) at cli/cppcheckexecutor.cpp:884
 #7  0x0000555555809c6a in CppCheckExecutor::check (this=0x7fffffffd8c0, argc=14, argv=0x7fffffffdc48) at cli/cppcheckexecutor.cpp:198
 #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));
                });
```
---
 lib/checkstl.cpp |  2 ++
 test/teststl.cpp | 14 ++++++++++++++
 2 files changed, 16 insertions(+)

diff --git a/lib/checkstl.cpp b/lib/checkstl.cpp
index 5bbbf70a0c7..123395b31e3 100644
--- a/lib/checkstl.cpp
+++ b/lib/checkstl.cpp
@@ -2036,6 +2036,8 @@ static const Token *singleMemberCallInScope(const Token *start, nonneg int varid
     if (!Token::findmatch(dotTok->tokAt(2), "%varid%", endStatement, varid))
         return nullptr;
     input = Token::Match(start->next(), "%var% . %name% ( %varid% )", varid);
+    if (!dotTok->astOperand1()) // incomplete code
+        return nullptr;
     if (isVariableChanged(dotTok->next(), endStatement, dotTok->astOperand1()->varId(), false, nullptr, true))
         return nullptr;
     return dotTok;
diff --git a/test/teststl.cpp b/test/teststl.cpp
index 99e861144eb..a20691fb549 100644
--- a/test/teststl.cpp
+++ b/test/teststl.cpp
@@ -3241,6 +3241,20 @@ class TestStl : public TestFixture {
               "    void shift() { EffectivityRangeData<int>::iterator it;  } \n"
               "};\n");
         ASSERT_EQUALS("", errout.str());
+
+        // test for crash in z3
+        check("struct explain::imp {\n"
+              "    solver &m_solver;\n"
+              "\n"
+              "    void project(var x, unsigned num, literal const *ls,\n"
+              "                 const scoped_literal_vector &result) {\n"
+              "        DEBUG_CODE(TRACE(\"nlsat\",\n"
+              "                         for (literal l\n"
+              "                              : result) { m_solver.display(tout << \" \", l); });\n"
+              "                        );\n"
+              "    }\n"
+              "};");
+        ASSERT_EQUALS("", errout.str());
     }
 
     void dereferenceInvalidIterator() {