Skip to content

Increase verification of 3C output in benchmark tests #428

Open
@mattmccutchen-cci

Description

@mattmccutchen-cci

Currently, the benchmark tests only check that 3C completes successfully (exit code 0). We should add more verification of the output. Ideas:

  • Without -alltypes, the output should compile.

  • With -alltypes, we could compare the output to a set of "reference" output files we maintain somewhere (similar to the manual evaluation procedure in the 3C document that we haven't used in a while). We have to think about how to make this useful: just having the tests fail every time the output changes may not be useful enough to justify the hassle.

    Another idea from Mike: Compare the count of each kind of checked pointer (similar to Tables 2-4 of the 3C paper submission (I won't paste the capability-granting link here)) and the number of Checked C type checking errors between the actual output and the reference output. If the count of checked pointers increases and the number of compile errors doesn't, that's probably good. We'd still have to decide how to translate that to a pass/fail status or how else to ensure we remember to monitor the quality of conversion.

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