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)

Metadata

Metadata

Labels

No labels
No labels

Type

No type

Fields

No fields configured for issues without a type.

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions