Skip to content

Changes to goto-harness documentation #5428

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
Merged
merged 1 commit into from
Jul 20, 2020
Merged

Changes to goto-harness documentation #5428

merged 1 commit into from
Jul 20, 2020

Conversation

NlightNFotis
Copy link
Contributor

This PR updates the goto-harness documentation with new usage examples, as the tool
has been updated to now produce completely different output (a .c file compared to a goto
binary).

By the way, this is dependent on #5412 and it will be rebased on top of develop once that
goes in. In reality, the diff for now is just the last commit.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

peterschrammel
peterschrammel approved these changes Jul 20, 2020
View reviewed changes
doc/architectural/goto-harness.md
The example above demonstrates the most simple case, which is roughly the same
---

The example above demonstrates the simplest case, which is roughly the same
as the entry point `cbmc` automatically generates for functions. However, the
`function-call` harness can also non-deterministically initialise global
Copy link
Member

Choose a reason for hiding this comment

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

⛏️

Suggested change
`function-call` harness can also non-deterministically initialise global
`function-call` harness can also non-deterministically initialize global

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I'd much rather not, especially since this bit hasn't been touched by this PR.

Unless you object to that strictly, of course.

@codecov
Copy link

codecov bot commented Jul 20, 2020

Codecov Report

Merging #5428 into develop will increase coverage by 0.02%.
The diff coverage is 70.00%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #5428      +/-   ##
===========================================
+ Coverage    68.21%   68.23%   +0.02%     
===========================================
  Files         1178     1178              
  Lines        97542    97550       +8     
===========================================
+ Hits         66537    66568      +31     
+ Misses       31005    30982      -23
Flag Coverage Δ
#cproversmt2 42.76% <ø> (ø)
#regression 65.40% <70.00%> (+0.02%) ⬆️
#unit 32.26% <ø> (ø)

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files Coverage Δ
src/goto-programs/name_mangler.h 100.00% <ø> (ø)
src/goto-programs/name_mangler.cpp 64.70% <50.00%> (ø)
src/goto-harness/recursive_initialization.cpp 90.17% <75.00%> (-0.28%) ⬇️
src/goto-instrument/goto_program2code.cpp 65.88% <0.00%> (+0.12%) ⬆️
src/goto-instrument/dump_c.cpp 78.42% <0.00%> (+3.83%) ⬆️
src/goto-programs/system_library_symbols.cpp 98.68% <0.00%> (+3.94%) ⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 069db73...1e9a74e. Read the comment docs.

1 similar comment
@codecov
Copy link

codecov bot commented Jul 20, 2020

Codecov Report

Merging #5428 into develop will increase coverage by 0.02%.
The diff coverage is 70.00%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #5428      +/-   ##
===========================================
+ Coverage    68.21%   68.23%   +0.02%     
===========================================
  Files         1178     1178              
  Lines        97542    97550       +8     
===========================================
+ Hits         66537    66568      +31     
+ Misses       31005    30982      -23
Flag Coverage Δ
#cproversmt2 42.76% <ø> (ø)
#regression 65.40% <70.00%> (+0.02%) ⬆️
#unit 32.26% <ø> (ø)

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files Coverage Δ
src/goto-programs/name_mangler.h 100.00% <ø> (ø)
src/goto-programs/name_mangler.cpp 64.70% <50.00%> (ø)
src/goto-harness/recursive_initialization.cpp 90.17% <75.00%> (-0.28%) ⬇️
src/goto-instrument/goto_program2code.cpp 65.88% <0.00%> (+0.12%) ⬆️
src/goto-instrument/dump_c.cpp 78.42% <0.00%> (+3.83%) ⬆️
src/goto-programs/system_library_symbols.cpp 98.68% <0.00%> (+3.94%) ⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 069db73...1e9a74e. Read the comment docs.

@NlightNFotis
Update the documentation for goto-harness.
8b31985 
This updates the usage instructions for goto-harness
to reflect the fact that it now produces a .c file,
and mark the memory snapshot harness as broken.
@NlightNFotis NlightNFotis force-pushed the goto_harness_docs_change branch from 1e9a74e to 8b31985 Compare July 20, 2020 14:46
@codecov
Copy link

codecov bot commented Jul 20, 2020 •
edited
Loading

Codecov Report

Merging #5428 into develop will not change coverage.
The diff coverage is n/a.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #5428   +/-   ##
========================================
  Coverage    68.21%   68.21%           
========================================
  Files         1178     1178           
  Lines        97550    97550           
========================================
  Hits         66542    66542           
  Misses       31008    31008
Flag Coverage Δ
#cproversmt2 42.76% <ø> (ø)
#regression 65.38% <ø> (ø)
#unit 32.26% <ø> (ø)

Flags with carried forward coverage won't be shown. Click here to find out more.

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update febb5cf...8b31985. Read the comment docs.

@NlightNFotis NlightNFotis merged commit a82c7d0 into diffblue:develop Jul 20, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@peterschrammel peterschrammel peterschrammel approved these changes

@danpoe danpoe danpoe approved these changes

@chrisr-diffblue chrisr-diffblue Awaiting requested review from chrisr-diffblue

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue Awaiting requested review from hannes-steffenhagen-diffblue

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@martin-cs martin-cs Awaiting requested review from martin-cs

@pkesseli pkesseli Awaiting requested review from pkesseli

@smowton smowton Awaiting requested review from smowton

@tautschnig tautschnig Awaiting requested review from tautschnig tautschnig is a code owner

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@NlightNFotis @peterschrammel @danpoe