Skip to content

Commit 397be23

Browse files
committed
Add STL regression tests
Adds additional regression tests for module calls and XOR instructions.
1 parent 46f2237 commit 397be23

File tree

6 files changed

+83
-2
lines changed

6 files changed

+83
-2
lines changed
Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
FUNCTION_BLOCK "Bool5"
2+
VERSION : 0.1
3+
VAR_INPUT
4+
in1 : Bool;
5+
END_VAR
6+
7+
VAR_OUTPUT
8+
out1 : Bool;
9+
END_VAR
10+
11+
12+
BEGIN
13+
NETWORK
14+
TITLE =
15+
CLR;
16+
X #in1;
17+
XN #in1;
18+
= #out1;
19+
CALL "__CPROVER_assert"
20+
( condition := #out1
21+
);
22+
23+
END_FUNCTION_BLOCK
24+
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.awl
3+
--function \"Bool5\"
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\*\* 0 of 1 failed \(1 iterations\)$
7+
^VERIFICATION SUCCESSFUL$
8+
--
9+
^warning: ignoring

regression/statement-list/Function_Call/main.awl renamed to regression/statement-list/Function_Call1/main.awl

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
FUNCTION_BLOCK "Function_Call"
1+
FUNCTION_BLOCK "Function_Call1"
22
VERSION : 0.1
33
VAR_INPUT
44
In1 : Bool;

regression/statement-list/Function_Call/test.desc renamed to regression/statement-list/Function_Call1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.awl
33
--show-parse-tree
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Name: "Function_Call"$
6+
^Name: "Function_Call1"$
77
^Version: 0[.]1$
88
^statement_list_call "__Function"$
99
^ param := In1$
Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
FUNCTION "Called_Function" : Void
2+
VERSION : 0.1
3+
VAR_INPUT
4+
Input : Bool;
5+
END_VAR
6+
7+
BEGIN
8+
NETWORK
9+
TITLE =
10+
11+
END_FUNCTION
12+
13+
14+
FUNCTION_BLOCK "Function_Call2"
15+
VERSION : 0.1
16+
VAR_INPUT
17+
In1 : Bool;
18+
END_VAR
19+
20+
BEGIN
21+
NETWORK
22+
TITLE =
23+
CALL "__CPROVER_assert"
24+
( condition := TRUE
25+
);
26+
27+
CALL "__CPROVER_assume"
28+
( condition := #In1
29+
);
30+
31+
CALL "__CPROVER_assert"
32+
( condition := #In1
33+
);
34+
35+
CALL "Called_Function"
36+
( Input := #In1
37+
);
38+
39+
END_FUNCTION_BLOCK
40+
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.awl
3+
--function \"Function_Call2\"
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

0 commit comments

Comments
 (0)