ACSL parser and translator improvements (#7)

ACSL parser and translator improvements.
uuverifiers · Oct 26, 2023 · d2c36a1 · d2c36a1
2 parents 9d3dc96 + 260139a
commit d2c36a1
Show file tree

Hide file tree

Showing 16 changed files with 630 additions and 453 deletions.
diff --git a/acsl-parser/Makefile b/acsl-parser/Makefile
@@ -1,7 +1,7 @@
 
 
 CUP = java_cup.Main
-CUPFLAGS = -expect 400 -locations
+CUPFLAGS = -expect 7 -locations
 
 JLEX = JLex.Main
 

diff --git a/acsl-parser/acsl-parser.jar b/acsl-parser/acsl-parser.jar
diff --git a/acsl-parser/acsl.cf b/acsl-parser/acsl.cf
diff --git a/regression-tests/acsl-contracts/contract11.hcc b/regression-tests/acsl-contracts/contract11.hcc
@@ -1,7 +1,7 @@
 /*@ 
   requires \valid(p, q);
-  ensures ((\result == *p) || (\result == *q));
-  ensures \result >= (*p);
+  ensures \result == *p || \result == *q;
+  ensures \result >= *p;
   ensures \result >= (*q);
 */
 int max(int* p, int* q) {

diff --git a/regression-tests/acsl-contracts/contract13.hcc b/regression-tests/acsl-contracts/contract13.hcc
@@ -1,7 +1,7 @@
 /*@
   requires \valid(p, q);
-  ensures ((\result == *p) || (\result == *q));
-  ensures \result >= (*p);
+  ensures \result == *p || \result == *q;
+  ensures \result >= *p;
   ensures \result >= (*q);
 */
 int max(int* p, int* q) {

diff --git a/regression-tests/acsl-contracts/contract14.hcc b/regression-tests/acsl-contracts/contract14.hcc
@@ -1,5 +1,5 @@
 /*@ 
-  ensures \forall int i; (i >= 0) ==> (i > \result);
+  ensures \forall int i; i >= 0 ==> i > \result;
 */
 int getNeg() {
   return -1;

diff --git a/regression-tests/acsl-contracts/contract2.hcc b/regression-tests/acsl-contracts/contract2.hcc
@@ -1,6 +1,6 @@
 /*@
-  requires (x >= 0) && (x <= 4);
-  ensures (\result >= 10) && (\result <= 14);
+  requires x >= 0 && x <= 4;
+  ensures \result >= 10 && \result <= 14;
 */
 int foo(int x) {
   return 12;

diff --git a/regression-tests/acsl-contracts/contract27.hcc b/regression-tests/acsl-contracts/contract27.hcc
@@ -3,7 +3,7 @@
 /*@
   requires \valid(a) && \valid(b);
   assigns  *a, *b;
-  ensures  (*a) == \old(*b);
+  ensures  *a == \old(*b);
   ensures  (*b) == \old(*a);
 */
 void swap(int* a, int* b) {

diff --git a/regression-tests/acsl-standalone/maxptr_unsafe.c b/regression-tests/acsl-standalone/maxptr_unsafe.c
@@ -1,7 +1,7 @@
 /*@ 
   requires \valid(p, q);
-  ensures ((\result == *p) || (\result == *q));
-  ensures \result >= (*p);
+  ensures \result == *p || \result == *q;
+  ensures \result >= *p;
   ensures \result >= (*q);
 */
 int foo(int* p, int* q) {

diff --git a/regression-tests/acsl-standalone/mc91_safe.c b/regression-tests/acsl-standalone/mc91_safe.c
@@ -1,6 +1,6 @@
 /*@
-  ensures ((n <= 100) ==> (\result == 91));
-  ensures ((n > 100) ==> (\result == (n-10)));
+  ensures n <= 100 ==> \result == 91;
+  ensures n > 100 ==> \result == n-10;
 */
 int foo(int n) {
   if (n > 100) {

diff --git a/regression-tests/runalldirs b/regression-tests/runalldirs
@@ -1,7 +1,5 @@
 #!/bin/sh
 
-set -e
-
 ./rundir horn-hcc-heap "" -assertNoVerify -dev -t:60
 ./rundir horn-hcc-array "" -assertNoVerify -dev -t:60
 ./rundir horn-bv "" -assert -dev -t:60

diff --git a/src/tricera/Main.scala b/src/tricera/Main.scala
@@ -498,8 +498,7 @@ class Main (args: Array[String]) {
                   processor(processedSolution)() // will process all predicates
               }
 
-              println("\nInferred ACSL annotations")
-              println("="*80)
+              var printedACSLHeader = false
               // line numbers in contract vars (e.g. x/1) are due to CCVar.toString
               for ((fun, ctx) <- contexts
                    if maybeEnc.isEmpty ||
@@ -515,6 +514,11 @@ class Main (args: Array[String]) {
                 val fPostWithArgs =
                   replaceArgs(fPost, ctx.postPredACSLArgNames)
 
+                if (!printedACSLHeader) {
+                  println("\nInferred ACSL annotations")
+                  println("=" * 80)
+                  printedACSLHeader = true
+                }
                 println("/* contracts for " + fun + " */")
                 println("/*@")
                 print(  "  requires "); println(fPreWithArgs + ";")
@@ -528,14 +532,21 @@ class Main (args: Array[String]) {
                     p._1.name.stripPrefix("inv_") == inv.pred.name).get._2
                   val fInvWithArgs =
                     replaceArgs(fInv, inv.argVars.map(_.name))
+                  if (!printedACSLHeader) {
+                    println("\nInferred ACSL annotations")
+                    println("=" * 80)
+                    printedACSLHeader = true
+                  }
                   println("\n/* loop invariant for the loop at line " +
                           srcInfo.line + " */")
                   println("/*@")
                   print(  "  loop invariant "); println(fInvWithArgs + ";")
                   println("*/")
                 }
               }
-              println("="*80 + "\n")
+              if (printedACSLHeader) {
+                println("=" * 80 + "\n")
+              }
             }
           case None =>
         }