diff --git a/src/solver/goblint_solver.ml b/src/solver/goblint_solver.ml index 0a264d7dea..946fff070b 100644 --- a/src/solver/goblint_solver.ml +++ b/src/solver/goblint_solver.ml @@ -5,6 +5,7 @@ The top-down solver family. *) module Td3 = Td3 +module Td_simplified = Td_simplified module TopDown = TopDown module TopDown_term = TopDown_term module TopDown_space_cache_term = TopDown_space_cache_term diff --git a/tests/regression/00-sanity/01-assert.t b/tests/regression/00-sanity/01-assert.t index 9b3b55f530..6dcebd71df 100644 --- a/tests/regression/00-sanity/01-assert.t +++ b/tests/regression/00-sanity/01-assert.t @@ -100,6 +100,18 @@ Test topdown solvers: dead: 2 total lines: 9 + $ goblint --enable warn.deterministic --set solver td_simplified 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) + [Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28) + [Warning][Deadcode] Function 'main' does not return + [Warning][Deadcode] Function 'main' has dead code: + on lines 13..14 (01-assert.c:13-14) + [Warning][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 2 + total lines: 9 + Test SLR solvers: