Skip to content

Commit

Permalink
Add cram test for YAML witness unrolled loop invariant (issue #1225)
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Feb 21, 2024
1 parent 2fb6b61 commit b010c16
Show file tree
Hide file tree
Showing 2 changed files with 31 additions and 0 deletions.
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
int main() {
int i = 0;
while (i < 10)
i++;
return 0;
}
25 changes: 25 additions & 0 deletions tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.t
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
$ goblint --set lib.activated '[]' --set exp.unrolling-factor 5 --enable ana.int.interval --enable witness.yaml.enabled 10-unrolled-loop-invariant.c
[Info] unrolling loop at 10-unrolled-loop-invariant.c:3:3-4:8 with factor 5
[Info][Deadcode] Logical lines of code (LLoC) summary:
live: 5
dead: 0
total lines: 5
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:3:10-3:16)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:3:10-3:16)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:3:10-3:16)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:3:10-3:16)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:3:10-3:16)
[Info][Witness] witness generation summary:
total generation entries: 4

$ cat witness.yml | grep -A 1 'value:'
value: (((((5 <= i && i <= 9) || i == 4) || i == 3) || i == 2) || i == 1) ||
i == 0
--
value: i == 10
format: c_expression
--
value: (((((5 <= i && i <= 10) || i == 4) || i == 3) || i == 2) || i == 1) ||
i == 0


0 comments on commit b010c16

Please sign in to comment.