Skip to content

Commit 05042f7

Browse files
Add CRAM test for __goblint_relation_track__ on formal parameters in justcil output
Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/1b1d4719-1b08-4c24-8446-31dbc3c31ecf Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
1 parent b223d14 commit 05042f7

2 files changed

Lines changed: 18 additions & 0 deletions

File tree

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
// CRAM
2+
int fun(int two) {
3+
int one;
4+
one = two + 1;
5+
if (one < two) {
6+
return 0;
7+
}
8+
return one;
9+
}
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
Autotune octagon should add __goblint_relation_track__ attribute to formal parameters, not just locals.
2+
3+
Attribute must appear on the formal parameter in the function signature:
4+
$ goblint --enable ana.autotune.enabled --set ana.autotune.activated[*] octagon --enable justcil --set dbg.justcil-printer clean --set lib.activated '[]' 40-autotune-octagon-formal.c 2>&1 | grep -c "two.*__goblint_relation_track__"
5+
1
6+
7+
Attribute must appear on the local variable declaration:
8+
$ goblint --enable ana.autotune.enabled --set ana.autotune.activated[*] octagon --enable justcil --set dbg.justcil-printer clean --set lib.activated '[]' 40-autotune-octagon-formal.c 2>&1 | grep -c "one.*__goblint_relation_track__"
9+
1

0 commit comments

Comments
 (0)