Skip to content

SV Comp local infrastructure fixes and improvements #25

Description

@nils-loose

SV-Comp

Remove reliance on log parsing (for context loss/ missing invocation tracking)

Potentially through a shared object passed with the trace. This should be stored in stats.json, the analysis can rely on this file per test case instead of log parsing.

Log storage/ analysis

For analysis some information is dated and some is parsed from the latests run.

  • Keep older logs and do not automatically overwrite
  • If log parsing stays use the correct log folder not the latest

Fix context loss vs. missing invocations inconsistencies

Currently there are some inconsistencies here.

The current states file should already contain this information per test case s.t. the analysis can rely on this per test case

New log folder structure:

- runs
- runs/run_<timestamp>
- runs/run_<timestamp>/logs
- runs/run_<timestamp>/results
- runs-debug/float/coral-33/run_<timestamp>/logs

Analyse script - summary

At the end of the analyse script print a concise scoring summary (Correct/ Failed/ Unk/ Error/ Timeout)

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Labels

No labels
No labels

Type

No type

Projects

No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions