Add documentation on goto-analyzer to the manual #6444
Conversation
martin-cs
requested review from
chrisr-diffblue,
kroening and
peterschrammel
as code owners
Codecov Report
@@ Coverage Diff @@
## develop #6444 +/- ##
===========================================
- Coverage 77.79% 76.01% -1.79%
===========================================
Files 1568 1527 -41
Lines 180317 164465 -15852
===========================================
- Hits 140285 125013 -15272
+ Misses 40032 39452 -580
Continue to review full report at Codecov.
|
| fix-point, then it will perform the task the user has chosen. | ||
|
|
||
| `--show` | ||
| : Displays a domain for every instruction in the GOTO binary. The |
There was a problem hiding this comment.
🦁 domain or abstract value?
There was a problem hiding this comment.
It displays the whole ai_domaint object. I am referring to this as the domain. In cases (in VSD) where I am talking about single abstract_objectt's I am calling them abstract values. Do you feel this is the correct terminology?
|
|
||
| `--show-on-source` | ||
| : The source code of the program is displayed line-by-line with the | ||
| abstract domains corresponding to each location displayed between |
There was a problem hiding this comment.
As with the original 🦁
|
|
||
| The histories described above are used to keep track of where in the | ||
| computation needs to be explored. The most precise option is to keep | ||
| one domain for every history but in some cases, to save memory and |
There was a problem hiding this comment.
As the original 🦁 above.
|
@peterschrammel thank you for the review and feedback; very helpful. What do you mean by ":lion:"? |
I think its a reference back to one of his previous comments "🦁 domain or abstract value?" - i.e. that comment applies everywhere else he's used the same emoij. |
|
Aaaaahhhhhhh; thank you @chrisr-diffblue |
|
Either that, or its a warning you are pulling a lions tail 😁 |
|
@martin-cs Thank you! |
martin-cs
force-pushed
the
feature/goto-analyzer-documentation
branch
from
d554aa8 to
45fe2ed
Compare
|
@peterschrammel only the 🦁 issues remain then I can merge. Let me know! |
martin-cs
force-pushed
the
feature/goto-analyzer-documentation
branch
from
45fe2ed to
2d2a3f3
Compare
|
@tautschnig @peterschrammel @chris-ryder The only failing tests are from the code coverage which has dropped because documentation seems to be included in the "percentage covered" metric. Do you mind if I just merge it? |
No concerns from my side! |
|
Thanks; I'll merge and if anyone knows how to remove documentation from the coverage count (or how we should test the documentation?) then I will have a go at fixing that in another PR. |
I have promised this to (in order of oldest promise) @tautschnig @remi-delmas-3000 @jimgrundy and @vmihalko . If any of you have a chance to look at this and say whether it is what you wanted / needed / hoped for then I would be very grateful.