Skip to content

Feature/correct instruction documentation #2193

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

Merged
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 19 additions & 6 deletions src/goto-programs/goto_program.h
Original file line number Diff line number Diff line change
Expand Up @@ -106,14 +106,20 @@ class goto_programt
/// respective fields in this class:
///
/// - GOTO:
/// if `guard` then goto `targets`
/// goto `targets` if and only if `guard` is true.
/// More than one target is deprecated. Its semantics was a
/// non-deterministic choice.
/// - RETURN:
/// Set the value returned by `code` (which shall be either nil or an
/// instance of code_returnt) and then jump to the end of the function.
/// Many analysis tools remove these instructions before they start.
/// - DECL:
/// Introduces a symbol denoted by the field `code` (an instance of
/// code_declt), the life-time of which is bounded by a corresponding DEAD
/// instruction.
/// instruction. Non-static symbols must be DECL'd before they are used.
/// - DEAD:
/// Ends the life of the symbol denoted by the field `code`.
/// After a DEAD instruction the symbol must be DECL'd again before use.
/// - FUNCTION_CALL:
/// Invoke the function denoted by field `code` (an instance of
/// code_function_callt).
Expand All @@ -124,27 +130,33 @@ class goto_programt
/// Execute the `code` (an instance of codet of kind ID_fence, ID_printf,
/// ID_array_copy, ID_array_set, ID_input, ID_output, ...).
/// - ASSUME:
/// Wait for `guard` to evaluate to true.
/// This thread of execution waits for `guard` to evaluate to true.
/// Assume does not "retro-actively" affect the thread or any ASSERTs.
/// - ASSERT:
/// Using ASSERT instructions is the one and only way to express
/// properties to be verified. Execution paths abort if `guard` evaluates
/// to false.
/// properties to be verified. An assertion is true / safe if `guard`
/// is true in all possible executions, otherwise it is false / unsafe.
/// The status of the assertion does not affect execution in any way.
/// - SKIP, LOCATION:
/// No-op.
/// - ATOMIC_BEGIN, ATOMIC_END:
/// When a thread executes ATOMIC_BEGIN, no thread other will be able to
/// execute any instruction until the same thread executes ATOMIC_END.
/// Concurrency is not supported by all analysis tools.
/// - END_FUNCTION:
/// Can only occur as the last instruction of the list.
/// Must occur as the last instruction of the list and nowhere else.
/// - START_THREAD:
/// Create a new thread and run the code of this function starting from
/// targets[0]. Quite often the instruction pointed by targets[0] will be
/// just a FUNCTION_CALL, followed by an END_THREAD.
/// Concurrency is not supported by all analysis tools.
/// - END_THREAD:
/// Terminate the calling thread.
/// Concurrency is not supported by all analysis tools.
/// - THROW:
/// throw `exception1`, ..., `exceptionN`
/// where the list of exceptions is extracted from the `code` field
/// Many analysis tools remove these instructions before they start.
/// - CATCH, when code.find(ID_exception_list) is non-empty:
/// Establishes that from here to the next occurrence of CATCH with an
/// empty list (see below) if
Expand All @@ -156,6 +168,7 @@ class goto_programt
/// - CATCH, when empty code.find(ID_exception_list) is empty:
/// clears all the catch clauses established as per the above in this
/// function?
/// Many analysis tools remove these instructions before they start.
class instructiont final
{
public:
Expand Down