Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

ACSL parser and translator improvements #7

Merged
merged 9 commits into from
Oct 26, 2023
Merged

ACSL parser and translator improvements #7

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
fb6a023
Start fix
zafer-esen Oct 6, 2023
4b28460
Merge branch 'master' into acsl-precedence-fix
zafer-esen Oct 23, 2023
1ed168e
Update grammar
zafer-esen Oct 25, 2023
094bd62
WIP: adapt the ACSL translator to the new grammar.
zafer-esen Oct 26, 2023
3c437b0
More fixes in the translator
zafer-esen Oct 26, 2023
542a084
More fixes in ACSLTranslator.
zafer-esen Oct 26, 2023
6217c07
Do not stop if any regression test fails.
zafer-esen Oct 26, 2023
679c798
Remove some parens in contracts in regression tests.
zafer-esen Oct 26, 2023
260139a
Small cleanup in ACSLTranslator
zafer-esen Oct 26, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion acsl-parser/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@


CUP = java_cup.Main
CUPFLAGS = -expect 400 -locations
CUPFLAGS = -expect 7 -locations

JLEX = JLex.Main

Expand Down
Binary file modified acsl-parser/acsl-parser.jar
View file
Open in desktop
Binary file not shown.
325 changes: 193 additions & 132 deletions acsl-parser/acsl.cf
View file
Open in desktop

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions regression-tests/acsl-contracts/contract11.hcc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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) {
Expand Down
4 changes: 2 additions & 2 deletions regression-tests/acsl-contracts/contract13.hcc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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) {
Expand Down
2 changes: 1 addition & 1 deletion regression-tests/acsl-contracts/contract14.hcc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*@
ensures \forall int i; (i >= 0) ==> (i > \result);
ensures \forall int i; i >= 0 ==> i > \result;
*/
int getNeg() {
return -1;
Expand Down
4 changes: 2 additions & 2 deletions regression-tests/acsl-contracts/contract2.hcc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
Expand Down
2 changes: 1 addition & 1 deletion regression-tests/acsl-contracts/contract27.hcc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down
4 changes: 2 additions & 2 deletions regression-tests/acsl-standalone/maxptr_unsafe.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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) {
Expand Down
4 changes: 2 additions & 2 deletions regression-tests/acsl-standalone/mc91_safe.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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) {
Expand Down
2 changes: 0 additions & 2 deletions regression-tests/runalldirs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,5 @@
#!/bin/sh

set -e
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A hidden change in this PR, regression tests will now continue until all tests are completed. This is better for getting feedback on exactly which tests failed.


./rundir horn-hcc-heap "" -assertNoVerify -dev -t:60
./rundir horn-hcc-array "" -assertNoVerify -dev -t:60
./rundir horn-bv "" -assert -dev -t:60
Expand Down
17 changes: 14 additions & 3 deletions src/tricera/Main.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ||
Expand All @@ -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 + ";")
Expand All @@ -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 =>
}
Expand Down
Loading
Loading