From b0243f91c6a3013d797b7a6cde8c59a605cfe0c4 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 16 Dec 2024 11:00:43 +0200 Subject: [PATCH] Disable broken two solver --- src/solver/sLR.ml | 2 +- tests/regression/00-sanity/01-assert.t | 115 ------------------------- 2 files changed, 1 insertion(+), 116 deletions(-) diff --git a/src/solver/sLR.ml b/src/solver/sLR.ml index 299bbbce52..03ba9307aa 100644 --- a/src/solver/sLR.ml +++ b/src/solver/sLR.ml @@ -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))) diff --git a/tests/regression/00-sanity/01-assert.t b/tests/regression/00-sanity/01-assert.t index cd8c4c06f8..9b3b55f530 100644 --- a/tests/regression/00-sanity/01-assert.t +++ b/tests/regression/00-sanity/01-assert.t @@ -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)