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

Update coverage properties #1209

Merged
merged 16 commits into from
Nov 4, 2020

Conversation

lembergerth
Copy link
Contributor

@lembergerth lembergerth commented Nov 3, 2020

[This PR was rebased against #1202 to get the correct XCSP verdicts.]

Over the course of the last year, a lot of tasks were fixed and a a lot of tasks were added.
Most of the time, people did not consider the coverage-* properties for these tasks, so let's add
them now.

Properties are added according to the criteria stated in #842:

  • Compiles, if __VERIFIER_X method definitions are provided,
  • No termination property or expected verdict for termination is true, and
  • Some _VERIFIER_nondet* method exists that is not only declared, but used in at least one other location

Compliance is checked and properties are added with the scripts found at
https://gist.github.com/lembergerth/1a1bf782931fb16af0d9e4bc1085a737 .

Ability to compile is checked with bin/prtest --compile-only,
PRTest version https://gitlab.com/sosy-lab/software/prtest/-/tree/cc9cc249

lembergerth and others added 12 commits October 30, 2020 13:02
…ore versatile script

Simplify large parts of the script used to create C files and
sv-benchmarks task definitions from XCSP3 task definitions.

Include binary for ./xcsp3_cpp_parser to avoid the manual step
of cloning the corresponding repository and building the binary.
Properly format assert(0)-changes, as well
- this is implied by the necessary formatting
of the benchmark tasks and can't be solved
in an easy way
Original version does not correctly convert
constraint-solving problems with extensional constraints
that are declared as conflicts
@holznerst
Copy link
Contributor

@skanav would you mind having a look at this PR?

@kfriedberger
Copy link
Member

kfriedberger commented Nov 4, 2020

Possible additional optional idea:

  • Add a CI-check that checks that all coverage-related benchmark tasks fulfill the above criteria.
  • Add a CI-check that checks that all not-coverage-related benchmark tasks do not fulfill the above criteria.

According to XCSP, these are open problems.
But we claim that they are safe (CPAchecker and CBMC report TRUE for most of them)
…-call

Over the course of the last year, a lot of tasks were fixed and a a lot of tasks were added.
Most of the time, people did not consider the coverage-* properties for these tasks, so let's add
them now.

Properties are added according to the criteria stated in !842:

    * Compiles, if __VERIFIER_X method definitions are provided,
    * No termination property or expected verdict for termination is true, and
    * Some _VERIFIER_nondet* method exists that is not only declared, but used in at least one other location

Compliance is checked and properties are added with the scripts found at
https://gist.github.com/lembergerth/1a1bf782931fb16af0d9e4bc1085a737 .

Ability to compile is checked with `bin/prtest --compile-only`,
PRTest version
https://gitlab.com/sosy-lab/software/prtest/-/tree/cc9cc249
@lembergerth
Copy link
Contributor Author

@kfriedberger or @skanav This PR is ready for review.

@skanav
Copy link
Contributor

skanav commented Nov 4, 2020

Looks good.

@skanav skanav self-requested a review November 4, 2020 18:11
@dbeyer dbeyer merged commit caf5411 into sosy-lab:master Nov 4, 2020
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.

5 participants