Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Support witnesses with ghost variables #653

Merged
merged 6 commits into from
Sep 9, 2024
Merged

Support witnesses with ghost variables #653

merged 6 commits into from
Sep 9, 2024

Commits on Sep 9, 2024

  1. Allow parsing witnesses with ghost variables

    @schuessf
    schuessf committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    6a3f776 View commit details
    Browse the repository at this point in the history

  2. Add support for the validation of witnesses with ghosts 

    The atomicity of the ghost update depends on the C-statement at the given location.
For now we only support locations where calls to these functions occur (we can extend this in the future):
* __VERIFIER_atomic_begin: The ghost update is inserted just after the call to add it to the atomic block
* __VERIFIER_atomic_end: The ghost update is inserted just before the call to add it to the atomic block
* pthread_create: The ghost update is inserted atomically just before the call
* pthread_mutex_lock / pthread_rwlock_rdlock / pthread_rwlock_wrlock: The ghost update is made atomically with the call to the locking function
* pthread_mutex_unlock / pthread_cond_wait / pthread_rwlock_unlock: The ghost update is made atomically with the call to the unlocking function
    @schuessf
    schuessf committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    729ef25 View commit details
    Browse the repository at this point in the history

  3. Allow writing ghost witnesses to YAML

    @schuessf
    schuessf committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    bf0d8c1 View commit details
    Browse the repository at this point in the history

  4. Add examples from VEWIT to regression tests 

    The format has changed since and the tests were slightly modified, since in the current version we only allow specific locations for ghost updates.
    @schuessf
    schuessf committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    0cff8b8 View commit details
    Browse the repository at this point in the history

  5. Split witness tests, use inlining for concurrent tests

    @schuessf
    schuessf committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    0e8c7e6 View commit details
    Browse the repository at this point in the history

  6. fix instrumentation of location invariants at labels

    @maul-esel @schuessf
    maul-esel authored and schuessf committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    d55e39c View commit details
    Browse the repository at this point in the history