Add more documentation for goto programs #2785
Conversation
danpoe
requested review from
kroening,
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
src/goto-programs/goto_functions.h
Outdated
| @@ -99,6 +101,7 @@ class goto_functionst | |||
| update_instructions_function(); | |||
| } | |||
|
|
|||
| /// Get the identifier of the entry point to a goto program | |||
src/goto-programs/goto_function.cpp
Outdated
| #include "goto_function.h" | ||
|
|
||
| /// Get the identifiers of the local variables declared in the function and the | ||
| /// identifiers of the paramters of the function. |
There was a problem hiding this comment.
Suggestion: implicitly document the parameters by referring to them in this sentence?
| code_typet type; | ||
|
|
||
| typedef std::vector<irep_idt> parameter_identifierst; | ||
|
|
||
| /// The identifiers of the parameters of this function |
There was a problem hiding this comment.
I've added a comment to #1695. I'll add a comment here to say that parameter_identifiers is currently always empty and that for now they should be retrieved from code_typet.
src/goto-programs/goto_function.h
Outdated
| @@ -17,13 +20,19 @@ Date: May 2018 | |||
|
|
|||
| #include "goto_program.h" | |||
|
|
|||
| /// A goto function, consisting of function type, function body, and parameter | |||
| /// identifiers. | |||
There was a problem hiding this comment.
A link to goto_programt should be provided to enable readers to figure out more details.
src/goto-programs/goto_functions.h
Outdated
| @@ -18,6 +18,7 @@ Date: June 2003 | |||
|
|
|||
| #include <util/cprover_prefix.h> | |||
|
|
|||
| /// A set of goto functions | |||
There was a problem hiding this comment.
Can I say "a collection of goto functions"? If we say set or map it could seem as if goto_functionst itself is a std::map or std::set.
src/goto-programs/goto_program.cpp
Outdated
| @@ -487,6 +487,9 @@ std::string as_string( | |||
| } | |||
| } | |||
|
|
|||
| /// Compute the loop numbers of the loops in the goto program. Every backwards | |||
There was a problem hiding this comment.
How about: "Assign each loop in the goto program a unique index."
src/goto-programs/goto_program.cpp
Outdated
| @@ -516,6 +519,15 @@ std::ostream &goto_programt::output( | |||
| return out; | |||
| } | |||
|
|
|||
| /// Compute the target numbers for the targets in the goto program. | |||
There was a problem hiding this comment.
How about: "Assign each control-flow join point in the goto program a unique index."
src/goto-programs/goto_program.h
Outdated
| @@ -613,6 +634,9 @@ class goto_programt | |||
| instructions.clear(); | |||
| } | |||
|
|
|||
| /// Get end function target | |||
There was a problem hiding this comment.
Instead of the term target it may be better to talk about "instruction iterators?" This applies throughout this PR.
src/goto-programs/goto_program.h
Outdated
| @@ -642,6 +669,18 @@ class goto_programt | |||
| void get_decl_identifiers(decl_identifierst &decl_identifiers) const; | |||
| }; | |||
|
|
|||
| /// Get control-flow successors of a given instruction. The instruction is | |||
There was a problem hiding this comment.
In my opinion this function is dangerous. Consequently I've created #2805.
danpoe
force-pushed
the
doc/goto-models
branch
4 times, most recently
from
1764ec4 to
5f8b77d
Compare
|
@tautschnig, @peterschrammel I've now addressed all the comments |
src/goto-programs/goto_program.cpp
Outdated
| @@ -604,7 +621,6 @@ void goto_programt::copy_from(const goto_programt &src) | |||
| compute_target_numbers(); | |||
| } | |||
|
|
|||
| // number them | |||
| bool goto_programt::has_assertion() const | |||
There was a problem hiding this comment.
Would you mind adding documentation (something along the lines of "Returns true if, and only if, the goto program includes an ASSERT instruction the guard of which is not trivially true.")
src/goto-programs/goto_program.cpp
Outdated
| @@ -614,6 +630,8 @@ bool goto_programt::has_assertion() const | |||
| return false; | |||
| } | |||
|
|
|||
| /// Compute for each instruction the set of instructions of which it is a | |||
| /// successor of. | |||
There was a problem hiding this comment.
I think "of which" should be removed. But check with someone whose first language is English.
danpoe
force-pushed
the
doc/goto-models
branch
from
5f8b77d to
e65f315
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: e65f315).
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
No description provided.