Skip to content

Enhance the expected testing framework #855

@zhassan-aws

Description

@zhassan-aws

Requested feature: With the recent switch to the new output format (#828), an assertion's result now spans multiple lines, e.g.:

RESULTS:
Check 1: foo.assertion.1
         - Status: FAILURE
         - Description: "assertion failed: x < 4"

Check 2: foo.assertion.2
         - Status: SUCCESS
         - Description: "assertion failed: x == 2"

However, the current expected test suite relies on the result being on a single line. So there is currently no way to check if the result of a specific assert was SUCCESS or FAILURE (a test that has an expected file with SUCCESS would pass if any check's result in that run was SUCCESS).

There is also no way to check that certain lines do not appear in the output.

We need to improve the expected testing framework to support the above requirements. One idea that was discussed is to add a mode to the CBMC result parser script that produces json with a well-defined schema. The compiletest tool will parse the json and provide a mechanism to query the parsed json for specific results.

Metadata

Metadata

Assignees

No one assigned

    Labels

    [C] InternalTracks some internal work. I.e.: Users should not be affected.

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions