Skip to content

Commit 4385b73

Browse files
committed
add td_simplified to Goblint_lib and cram test 00/01
1 parent 4755400 commit 4385b73

File tree

2 files changed

+13
-0
lines changed

2 files changed

+13
-0
lines changed

src/solver/goblint_solver.ml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55
The top-down solver family. *)
66

77
module Td3 = Td3
8+
module Td_simplified = Td_simplified
89
module TopDown = TopDown
910
module TopDown_term = TopDown_term
1011
module TopDown_space_cache_term = TopDown_space_cache_term

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -100,6 +100,18 @@ Test topdown solvers:
100100
dead: 2
101101
total lines: 9
102102

103+
$ goblint --enable warn.deterministic --set solver td_simplified 01-assert.c
104+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
105+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
106+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
107+
[Warning][Deadcode] Function 'main' does not return
108+
[Warning][Deadcode] Function 'main' has dead code:
109+
on lines 13..14 (01-assert.c:13-14)
110+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
111+
live: 7
112+
dead: 2
113+
total lines: 9
114+
103115

104116
Test SLR solvers:
105117

0 commit comments

Comments
 (0)