Skip to content

--stop-on-fail suppresses output of proof objectives status when analysis is successfull. #7059

Closed
@remi-delmas-3000

Description

@remi-delmas-3000

The terminal output does not print individual PO statuses when --stop-on-fail is used, making it hard to see what was actually analysed.

CBMC version: 5.62
Operating system: Linux, macOS
Exact command line resulting in the issue: cbmc --stop-on-fail main.c
What behaviour did you expect: status of POs printed in terminal
What happened instead: no status printed

int main()
{
  int x;
  assert((x==0) ==> (2*x == 0));
}
❯ cbmc --stop-on-fail main.c
CBMC version 5.62.0 (cbmc-5.62.0-52-ga1d9f75c2d-dirty) 64-bit x86_64 macos
Parsing main.c
Converting
Type-checking main
file main.c line 4 function main: function 'assert' is not declared
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.000902692s
size of program expression: 37 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 1.3229e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00036133s
Running propositional reduction
Post-processing
Runtime Post-process: 3.4564e-05s
Solving with MiniSAT 2.2.1 with simplifier
241 variables, 33 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 6.6318e-05s
Runtime decision procedure: 0.000482911s
VERIFICATION SUCCESSFUL

Without stop on fail:

❯ cbmc main.c
CBMC version 5.62.0 (cbmc-5.62.0-52-ga1d9f75c2d-dirty) 64-bit x86_64 macos
Parsing main.c
Converting
Type-checking main
file main.c line 4 function main: function 'assert' is not declared
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.000974558s
size of program expression: 37 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 1.3696e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000350669s
Running propositional reduction
Post-processing
Runtime Post-process: 2.3313e-05s
Solving with MiniSAT 2.2.1 with simplifier
241 variables, 33 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 4.2389e-05s
Runtime decision procedure: 0.000427057s

** Results:
main.c function main
[main.assertion.1] line 4 assertion x == 0 ==> 2 * x == 0: SUCCESS

** 0 of 1 failed (1 iterations)
VERIFICATION SUCCESSFUL

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions