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.

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

Update coverage properties in task definitions #774

Merged
merged 2 commits into from Jan 10, 2019

Conversation

Projects
None yet
3 participants
@lembergerth
Copy link
Contributor

commented Jan 10, 2019

Add coverage properties to tasks that compile now and haven't compiled
before, and remove coverage properties from tasks with a property "termination = false".

The first is possible thanks to large improvements to the sv-benchmark set.
The second is necessary because test-suite generation and coverage measurements for tasks that do not terminate are questionable for now.

With this PR, the following tasks have properties coverage-branches etc.:

  1. Compile with gcc, if a harness for the special __VERIFIER_ methods (and none other!) is provided.
  2. Contain at least one call to a nondeterministic function __VERIFIER_nondet_X
  3. Do not have property "termination = false".

And the following tasks have property coverage-error-call:

  1. Fulfill above conditions
  2. Do have property "unreach-call = false"

I'm happy about feedback.

Update coverage properties in task definitions
Add coverage properties to tasks that compile now and haven't compiled
before, and remove coverage properties from tasks
with a property "termination = false".

@lembergerth lembergerth changed the title Update coverage properties in task definitions [WIP] Update coverage properties in task definitions Jan 10, 2019

@lembergerth

This comment has been minimized.

Copy link
Contributor Author

commented Jan 10, 2019

I've added Work-In-Progress to the PR's title, as some tasks might have been missed due to missing libraries on some of our workers.
There are probably some additional tasks that will get the coverage-property after re-running the experiments on a fixed set of working workers.

@lembergerth lembergerth changed the title [WIP] Update coverage properties in task definitions Update coverage properties in task definitions Jan 10, 2019

@lembergerth

This comment has been minimized.

Copy link
Contributor Author

commented Jan 10, 2019

The tasks should be complete now, according to the selection criteria stated above.

@dbeyer

dbeyer approved these changes Jan 10, 2019

Copy link
Member

left a comment

Thanks a lot for this improvement.
The changes were requested in the context of Test-Comp.

@dbeyer dbeyer merged commit 88000d8 into sosy-lab:master Jan 10, 2019

1 check passed

continuous-integration/travis-ci/pr The Travis CI build passed
Details
@animeshbchowdhury

This comment has been minimized.

Copy link
Contributor

commented Jan 15, 2019

Hi,

I have a question. From testcomp perspective, is it an underlying assumption that program should always terminate irrespective of any test-input provided ?

I thought programs which terminate depending on test/user input would be present. A clarification would be really helpful in this matter.

Best Regards,
Animesh

@lembergerth

This comment has been minimized.

Copy link
Contributor Author

commented Jan 16, 2019

Hi Animesh,

our current decision is to exclude all programs that do not terminate for at least one input.
Reason: We measure coverage with gcov, and gcov fails to write coverage information if the program run
is aborted. Since we abort a program run after a certain time limit is reached, this would lead to incorrect/incomplete coverage information.

Best,
Thomas

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.