Skip to content

Commit b0243f9

Browse files
sim642sim642
committed
Disable broken two solver
1 parent 4a9b52f commit b0243f9

File tree

2 files changed

+1
-116
lines changed

2 files changed

+1
-116
lines changed

‎src/solver/sLR.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -527,7 +527,7 @@ let _ =
527527
Selector.add_solver ("widen2", (module PostSolver.EqIncrSolverFromEqSolver (W2)));
528528
Selector.add_solver ("widen3", (module PostSolver.EqIncrSolverFromEqSolver (W3)));
529529
let module S2 = TwoPhased (struct let ver = 1 end) in
530-
Selector.add_solver ("two", (module PostSolver.EqIncrSolverFromEqSolver (S2))); (* TODO: broken even on 00-sanity/01-assert *)
530+
(* Selector.add_solver ("two", (module PostSolver.EqIncrSolverFromEqSolver (S2))); (* TODO: broken even on 00-sanity/01-assert *) *)
531531
let module S1 = Make (struct let ver = 1 end) in
532532
Selector.add_solver ("new", (module PostSolver.EqIncrSolverFromEqSolver (S1)));
533533
Selector.add_solver ("slr+", (module PostSolver.EqIncrSolverFromEqSolver (S1)))

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

Lines changed: 0 additions & 115 deletions
Original file line numberDiff line numberDiff line change
@@ -139,121 +139,6 @@ Test SLR solvers:
139139
dead: 2
140140
total lines: 9
141141

142-
$ goblint --enable warn.deterministic --set solver two 01-assert.c
143-
[Error] Fixpoint not reached at L:entry state of main (299) on 01-assert.c:4:1-15:1
144-
Solver computed:
145-
bot
146-
Right-Hand-Side:
147-
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[expRelation:(),
148-
mallocWrapper:(wrapper call:Unknown node, unique calls:{}),
149-
base:({
150-
}, {}, {}, {}),
151-
threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)),
152-
threadflag:Singlethreaded,
153-
threadreturn:true,
154-
escape:{},
155-
mutexEvents:(),
156-
access:(),
157-
mutex:(lockset:{}, multiplicity:{}),
158-
race:(),
159-
mhp:(),
160-
assert:(),
161-
pthreadMutexType:()], map:{})}
162-
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[expRelation:(),
163-
mallocWrapper:(wrapper call:Unknown node, unique calls:{}),
164-
base:({
165-
}, {}, {}, {}),
166-
threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)),
167-
threadflag:Singlethreaded,
168-
threadreturn:true,
169-
escape:{},
170-
mutexEvents:(),
171-
access:(),
172-
mutex:(lockset:{}, multiplicity:{}),
173-
race:(),
174-
mhp:(),
175-
assert:(),
176-
pthreadMutexType:()], map:{})} instead of bot
177-
178-
[Error] Fixpoint not reached at L:node 1 "success = 1;" on 01-assert.c:5:7-5:18
179-
Solver computed:
180-
bot
181-
Right-Hand-Side:
182-
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code
183-
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code instead of bot
184-
185-
[Error] Fixpoint not reached at L:node 2 "silence = 1;" on 01-assert.c:6:7-6:18
186-
Solver computed:
187-
bot
188-
Right-Hand-Side:
189-
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code
190-
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code instead of bot
191-
192-
[Error] Fixpoint not reached at L:node 3 "fail = 0;" on 01-assert.c:7:7-7:15
193-
Solver computed:
194-
bot
195-
Right-Hand-Side:
196-
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code
197-
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code instead of bot
198-
199-
[Error] Fixpoint not reached at L:node 4 "__goblint_assert(success);" on 01-assert.c:10:3-10:28
200-
Solver computed:
201-
bot
202-
Right-Hand-Side:
203-
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code
204-
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code instead of bot
205-
206-
[Error] Fixpoint not reached at L:node 5 "__goblint_assert(unknown == 4);" on 01-assert.c:11:3-11:33
207-
Solver computed:
208-
bot
209-
Right-Hand-Side:
210-
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code
211-
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code instead of bot
212-
213-
[Error] Fixpoint not reached at L:node 6 "__goblint_assert(fail);" on 01-assert.c:12:3-12:25
214-
Solver computed:
215-
bot
216-
Right-Hand-Side:
217-
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code
218-
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code instead of bot
219-
220-
[Error] Fixpoint not reached at L:node 7 "return (0);" on 01-assert.c:13:10-13:11
221-
Solver computed:
222-
bot
223-
Right-Hand-Side:
224-
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code
225-
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code instead of bot
226-
227-
[Error] Fixpoint not reached at L:node 9 "__goblint_assert(silence);" on 01-assert.c:14:3-14:28
228-
Solver computed:
229-
bot
230-
Right-Hand-Side:
231-
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code
232-
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code instead of bot
233-
234-
[Error] Fixpoint not reached at L:node -299 "return;" on 01-assert.c:15:1-15:1
235-
Solver computed:
236-
bot
237-
Right-Hand-Side:
238-
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code
239-
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code instead of bot
240-
241-
[Error] Fixpoint not reached at L:call of main (299) on 01-assert.c:4:1-15:1
242-
Solver computed:
243-
bot
244-
Right-Hand-Side:
245-
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code
246-
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code instead of bot
247-
248-
[Warning][Deadcode] Function 'main' does not return
249-
[Warning][Deadcode] Function 'main' is uncalled: 8 LLoC (01-assert.c:4:1-15:1)
250-
[Info][Deadcode] Logical lines of code (LLoC) summary:
251-
live: 0
252-
dead: 8 (8 in uncalled functions)
253-
total lines: 8
254-
[Error][Unsound] Fixpoint not reached
255-
[3]
256-
257142
$ goblint --enable warn.deterministic --set solver new 01-assert.c
258143
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
259144
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)

0 commit comments

Comments
 (0)