Skip to content
This repository has been archived by the owner on Oct 14, 2022. It is now read-only.

Introduce entry type 'location_invariant' for YAML-based witnesses. #59

Open
wants to merge 1 commit into
base: main
Choose a base branch
from

Conversation

SvenUmbricht
Copy link
Contributor

This PR introduces a new entry type for YAML-based witnesses that describes location invariants.

@SvenUmbricht SvenUmbricht requested a review from dbeyer May 18, 2022 11:03
@SvenUmbricht
Copy link
Contributor Author

SvenUmbricht commented May 18, 2022

Something that still needs to be discussed is how the producer section is currently only refering to "tools", even though an entry could be created by a human as well (true for both location- and loop invariants). The simple fix of replacing "tool" by something like "e.g. the tool" which we discussed previously does not work, because some fields (version/configuration/commandline) do not make sense if the witness was created by hand.

| `producer` | assoc. array | [see below](#producer-1) | Tool that produced the entry. |
| `task` | assoc. array | [see below](#task-1) | Verification task during which the entry was produced. |

##### producer
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It might get a bit redundant if we start copying sections like this. I would rather have the description refactored such that we have a section for common keys like producer and then just point to that section for the different entry types.

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here's a radical idea: ditch the hand-written Markdown altogether and have everything in a nice JSON schema, see #61.

@sim642 sim642 mentioned this pull request Jun 13, 2022
5 tasks
sim642 added a commit to goblint/sv-witnesses that referenced this pull request Sep 2, 2022
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants