Skip to content

Commit

Permalink
Disable broken two solver
Browse files Browse the repository at this point in the history
  • Loading branch information
@sim642
sim642 committed Dec 16, 2024
1 parent 4a9b52f commit b0243f9
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 116 deletions.
2 changes: 1 addition & 1 deletion src/solver/sLR.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -527,7 +527,7 @@ let _ =
Selector.add_solver ("widen2", (module PostSolver.EqIncrSolverFromEqSolver (W2)));
Selector.add_solver ("widen3", (module PostSolver.EqIncrSolverFromEqSolver (W3)));
let module S2 = TwoPhased (struct let ver = 1 end) in
Selector.add_solver ("two", (module PostSolver.EqIncrSolverFromEqSolver (S2))); (* TODO: broken even on 00-sanity/01-assert *)
(* Selector.add_solver ("two", (module PostSolver.EqIncrSolverFromEqSolver (S2))); (* TODO: broken even on 00-sanity/01-assert *) *)
let module S1 = Make (struct let ver = 1 end) in
Selector.add_solver ("new", (module PostSolver.EqIncrSolverFromEqSolver (S1)));
Selector.add_solver ("slr+", (module PostSolver.EqIncrSolverFromEqSolver (S1)))
Expand Down
115 changes: 0 additions & 115 deletions tests/regression/00-sanity/01-assert.t
View file
Original file line number Diff line number Diff line change
Expand Up @@ -139,121 +139,6 @@ Test SLR solvers:
dead: 2
total lines: 9

$ goblint --enable warn.deterministic --set solver two 01-assert.c
[Error] Fixpoint not reached at L:entry state of main (299) on 01-assert.c:4:1-15:1
Solver computed:
bot
Right-Hand-Side:
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[expRelation:(),
mallocWrapper:(wrapper call:Unknown node, unique calls:{}),
base:({
}, {}, {}, {}),
threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)),
threadflag:Singlethreaded,
threadreturn:true,
escape:{},
mutexEvents:(),
access:(),
mutex:(lockset:{}, multiplicity:{}),
race:(),
mhp:(),
assert:(),
pthreadMutexType:()], map:{})}
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[expRelation:(),
mallocWrapper:(wrapper call:Unknown node, unique calls:{}),
base:({
}, {}, {}, {}),
threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)),
threadflag:Singlethreaded,
threadreturn:true,
escape:{},
mutexEvents:(),
access:(),
mutex:(lockset:{}, multiplicity:{}),
race:(),
mhp:(),
assert:(),
pthreadMutexType:()], map:{})} instead of bot

[Error] Fixpoint not reached at L:node 1 "success = 1;" on 01-assert.c:5:7-5:18
Solver computed:
bot
Right-Hand-Side:
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code instead of bot

[Error] Fixpoint not reached at L:node 2 "silence = 1;" on 01-assert.c:6:7-6:18
Solver computed:
bot
Right-Hand-Side:
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code instead of bot

[Error] Fixpoint not reached at L:node 3 "fail = 0;" on 01-assert.c:7:7-7:15
Solver computed:
bot
Right-Hand-Side:
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code instead of bot

[Error] Fixpoint not reached at L:node 4 "__goblint_assert(success);" on 01-assert.c:10:3-10:28
Solver computed:
bot
Right-Hand-Side:
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code instead of bot

[Error] Fixpoint not reached at L:node 5 "__goblint_assert(unknown == 4);" on 01-assert.c:11:3-11:33
Solver computed:
bot
Right-Hand-Side:
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code instead of bot

[Error] Fixpoint not reached at L:node 6 "__goblint_assert(fail);" on 01-assert.c:12:3-12:25
Solver computed:
bot
Right-Hand-Side:
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code instead of bot

[Error] Fixpoint not reached at L:node 7 "return (0);" on 01-assert.c:13:10-13:11
Solver computed:
bot
Right-Hand-Side:
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code instead of bot

[Error] Fixpoint not reached at L:node 9 "__goblint_assert(silence);" on 01-assert.c:14:3-14:28
Solver computed:
bot
Right-Hand-Side:
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code instead of bot

[Error] Fixpoint not reached at L:node -299 "return;" on 01-assert.c:15:1-15:1
Solver computed:
bot
Right-Hand-Side:
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code instead of bot

[Error] Fixpoint not reached at L:call of main (299) on 01-assert.c:4:1-15:1
Solver computed:
bot
Right-Hand-Side:
HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code
Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):Dead code instead of bot

[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' is uncalled: 8 LLoC (01-assert.c:4:1-15:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
live: 0
dead: 8 (8 in uncalled functions)
total lines: 8
[Error][Unsound] Fixpoint not reached
[3]

$ goblint --enable warn.deterministic --set solver new 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
Expand Down

0 comments on commit b0243f9

Please sign in to comment.