Skip to content

Commit a1d437e

Browse files
committed
td_simplified_ref: Sanity test
1 parent 0a6e558 commit a1d437e

File tree

1 file changed

+12
-0
lines changed

1 file changed

+12
-0
lines changed

tests/regression/00-sanity/01-assert.t

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -112,6 +112,18 @@ Test topdown solvers:
112112
dead: 2
113113
total lines: 9
114114

115+
$ goblint --enable warn.deterministic --set solver td_simplified_ref 01-assert.c
116+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
117+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
118+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
119+
[Warning][Deadcode] Function 'main' does not return
120+
[Warning][Deadcode] Function 'main' has dead code:
121+
on lines 13..14 (01-assert.c:13-14)
122+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
123+
live: 7
124+
dead: 2
125+
total lines: 9
126+
115127

116128
Test SLR solvers:
117129

0 commit comments

Comments
 (0)