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: