Fixes in tri-pp, bump up its version

build.sbt

@@ -42,7 +42,7 @@ lazy val acslParser = (project in file("acsl-parser")).
 
 lazy val pp = taskKey[Unit]("")
 pp := {
-  val f = url("https://github.com/zafer-esen/tri-pp/releases/download/v0.1.2/tri-pp")
+  val f = url("https://github.com/zafer-esen/tri-pp/releases/download/v0.1.3/tri-pp")
   f #> file("tri-pp") !
 }
 def addExecutePermissions(file : File) {

regression-tests/horn-hcc-heap/Answers

@@ -249,3 +249,9 @@ SAFE
 
 stack-ptr-bug-1.c
 UNKNOWN (Unsupported C fragment. 11:10 Stack pointers in combination with heap pointers)
+
+sizeof-bug-1-true.c
+SAFE
+
+sizeof-bug-2-true.c
+SAFE

regression-tests/horn-hcc-heap/runtests

@@ -10,7 +10,7 @@ for name in $TESTS; do
     $LAZABS -cex -abstract:off "$@" $name 2>&1 | grep -v 'at '
 done
 
-VALID_DEREF_TESTS="stack-ptr-bug-1.c"
+VALID_DEREF_TESTS="stack-ptr-bug-1.c sizeof-bug-1-true.c sizeof-bug-2-true.c"
 
 for name in $VALID_DEREF_TESTS; do
     echo

regression-tests/horn-hcc-heap/sizeof-bug-1-true.c

@@ -0,0 +1,19 @@
+#include <stdlib.h>
+
+struct S1
+{
+  struct S1* f1;
+};
+
+struct S2
+{
+  struct S1* f2;
+};
+
+int main()
+{
+  struct S2 s2;
+  s2.f2 = malloc(sizeof(*s2.f2));
+  s2.f2->f1 = s2.f2;
+  return 0;
+}

regression-tests/horn-hcc-heap/sizeof-bug-2-true.c

@@ -0,0 +1,21 @@
+#include <stdlib.h>
+
+struct S1
+{
+  struct S1* f1;
+};
+
+struct S2
+{
+  struct S1* f2;
+};
+
+int main()
+{
+  struct S2 s2;
+  struct S1 **p = malloc(sizeof(s2.f2)); // p is S1**, s2.f2 is S1*
+  *p = malloc(sizeof(*s2.f2));  // *p is S1*, *s2.f2 is S1
+  s2.f2 = *p;
+  s2.f2->f1 = *p; // lhs is S1*, rhs is also S1*
+  return 0;
+}

src/tricera/Main.scala

@@ -291,7 +291,7 @@ class Main (args: Array[String]) {
 
       if (logPPLevel > 0)
         Console.withOut(outStream) {
-          println("=" * 80 + "\nPreprocessor warnings and errors\n")
+          println("=" * 80 + "\nTriCera's preprocessor (tri-pp) warnings and errors\n")
         }
 
       val pp = new TriCeraPreprocessor(cppFileName,
@@ -300,17 +300,16 @@ class Main (args: Array[String]) {
         quiet = logPPLevel == 0,
         entryFunction = TriCeraParameters.get.funcName)
       if (logPPLevel > 0) Console.withOut(outStream) {
-        println("\n\nEnd of preprocessor warnings and errors")
+        println("\n\nEnd of TriCera's preprocessor (tri-pp) warnings and errors")
         println("=" * 80)
       }
 
       if (pp.hasError && logPPLevel > 0)
-        Util.warn("The preprocessor (LLVM) reported an error in the" +
-          " input file, This might be due to TriCera accepting a non-standard" +
-          " subset of the C language, or due to an actual error in the " +
-          "input program. You can safely ignore this warning if it is" +
-          " the former. You can print preprocessor warnings and errors " +
-          "using the -warnPP option.")
+        Util.warn(
+          """The preprocessor tri-pp (LLVM) reported an error in the input file, This might
+            |be due to TriCera accepting a non-standard subset of the C language, or
+            |due to an actual error in the input program. You can safely ignore this
+            |warning if it is the former.""".stripMargin)
 
       if (printPP) {
         val src = scala.io.Source.fromFile(preprocessedFile)
@@ -332,7 +331,16 @@ class Main (args: Array[String]) {
       //            Nil, false,  0, preprocessTimer.s)
       //throw new MainException("Input file has unsupported C features " +
       //  "(e.g. varargs)") // todo: more detail
-      preprocessedFile.getAbsolutePath
+      if(preprocessedFile.length() == 0 && pp.hasError) {
+        Util.warn(
+          """TriCera preprocessor (tri-pp) returned an empty file - attempting
+            |to continue without it. Use option -logPP:2 to display what went
+            |wrong, use option -noPP to disable the preprocessor and this warning.
+            |""".stripMargin)
+        cppFileName
+      } else {
+        preprocessedFile.getAbsolutePath
+      }
     }
     preprocessTimer.stop()
 
@@ -455,7 +463,12 @@ class Main (args: Array[String]) {
       if (propertiesToCheck.forall(propertyToExpected.contains)) {
         if (propertyToExpected.filter(
           pair => propertiesToCheck.contains(pair._1)).forall(_._2)) "sat"
-        else "unsat"
+        else {
+          if (useMemCleanupForMemTrack &&
+              propertiesToCheck.contains(properties.MemValidTrack))
+            "unknown"
+          else "unsat"
+        }
       } else "unknown"
 
     val smtFileName = if (splitProperties) {

src/tricera/concurrency/CCReader.scala

@@ -3466,14 +3466,16 @@ private def collectVarDecls(dec                    : Dec,
                   (getType(exp.exp_2.asInstanceOf[Ebytestype]), eval(e))
                 case _ =>
                   throw new UnsupportedCFragmentException(
-                    "Unsupported alloc expression: " + (printer print exp))
+                    getLineStringShort(srcInfo) +
+                    " Unsupported alloc expression: " + (printer print exp))
               }
             //case exp : Evar => // allocation in bytes
             case e : Econst => // allocation in bytes
               (CCInt, eval(e)) // todo: add support for char?
 
             case _ => throw new UnsupportedCFragmentException(
-              "Unsupported alloc expression: " + (printer print exp))
+              getLineStringShort(srcInfo) +
+              " Unsupported alloc expression: " + (printer print exp))
           }
 
           val arrayLoc = name match {

src/tricera/params/TriCeraParameters.scala

@@ -364,7 +364,8 @@ class TriCeraParameters extends GlobalParameters {
     |TriCera preprocessor:
     |-printPP           Print the output of the TriCera preprocessor to stdout
     |-dumpPP            Dump the output of the TriCera preprocessor to file (input file name + .tri)
-    |-logPP:n           Display TriCera preprocessor warnings and errors with verbosity n (currently 0 <= n <= 2)
+    |-logPP:n           Display TriCera preprocessor warnings and errors with verbosity n.
+    |                     (0 <= n <= 2, default: 0)
     |-noPP              Turn off the TriCera preprocessor (typedefs are not allowed in this mode)
 
     |Debugging: