sv-witnesses

sv-witnesses copied to clipboard

Reconsider the `architecture` description in the witness graphml files

1

For the task definition files we now have a consistent filed named `data_model` that contains either `ILP32` or `LP64`: https://github.com/sosy-lab/sv-benchmarks#task-definitions > - options: parameters that are relevant for verification or...

MartinSpiessl

Example for a correctness witness contains forbidden data key `control`

13

The example [multivar_true-unreach-call1.graphml](https://github.com/sosy-lab/sv-witnesses/blob/master/multivar_true-unreach-call1.graphml) for a correctness witness in this repository contains control annotations like the following: [!(x < 1024)] 12 305 condition-false According to the `README.md`, the data key `control`...

MartinSpiessl

This way it would be easier for users to execute the witnes linter against their witnesses to check whether they are conformant with the spec

MartinSpiessl

Feature request: Python API

2

Hello sv-witnesses developers, I was wondering if it makes sense to provide Python APIs (e.g., witness node classes with methods to create/manipulate them). I think it would benefit the users...

shaobo-he