Skip to content

Improvement suggestions for CBMC output #4013

Open
@peterschrammel

Description

@peterschrammel
  • Runtime decision procedure -> Decision procedure runtime
  • Measure duration for different phases separately: symex, conversion, solving
  • goto checker iterations should be JSON/XML formatted
  • fix incomplete plain text tests output in c_test_input_generator for multiple i/o values Add cover goals verifier [blocks: 3969] #3968 (comment)
  • reconsider removing special cases when traces are output or not in JSON/XML vs plain text

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions