Skip to content

Commit 5656450

Browse files
MatWisetautschnig
authored andcommitted
Add regression test for STL jumps
1 parent f985d81 commit 5656450

File tree

2 files changed

+45
-0
lines changed

2 files changed

+45
-0
lines changed
Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
FUNCTION_BLOCK "Main"
2+
VERSION : 0.1
3+
VAR_TEMP
4+
temp1 : Bool;
5+
temp2 : Bool;
6+
END_VAR
7+
BEGIN
8+
NETWORK
9+
TITLE =
10+
SET;
11+
= temp1;
12+
= temp2;
13+
JU lab0;
14+
CALL "__CPROVER_assert"
15+
( condition := FALSE
16+
);
17+
lab0: SET;
18+
lab1: A temp1;
19+
A temp2;
20+
NOT;
21+
= temp2;
22+
A temp2;
23+
24+
JCN lab1;
25+
CALL "__CPROVER_assert"
26+
( condition := #temp2
27+
);
28+
29+
JC lab2;
30+
CALL "__CPROVER_assert"
31+
( condition := FALSE
32+
);
33+
34+
lab2: NOP 0;
35+
36+
END_FUNCTION_BLOCK
37+
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.awl
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

0 commit comments

Comments
 (0)