cprover
|
Go to the source code of this file.
Classes | |
class | code_assignt |
A codet representing an assignment in the program. More... | |
class | code_deadt |
A codet representing the removal of a local variable going out of scope. More... | |
class | code_declt |
A codet representing the declaration of a local variable. More... | |
class | code_function_callt |
codet representation of a function call statement. More... | |
class | code_inputt |
A codet representing the declaration that an input of a particular description has a value which corresponds to the value of a given expression (or expressions). More... | |
class | code_outputt |
A codet representing the declaration that an output of a particular description has a value which corresponds to the value of a given expression (or expressions). More... | |
class | code_returnt |
codet representation of a "return from a function" statement. More... | |
|
inline |
Definition at line 100 of file goto_instruction_code.h.
|
inline |
Definition at line 170 of file goto_instruction_code.h.
|
inline |
Definition at line 235 of file goto_instruction_code.h.
|
inline |
Definition at line 367 of file goto_instruction_code.h.
|
inline |
Definition at line 428 of file goto_instruction_code.h.
|
inline |
Definition at line 474 of file goto_instruction_code.h.
|
inline |
Definition at line 517 of file goto_instruction_code.h.
|
inline |
Builds a code_function_callt to __CPROVER_havoc_slice(p, size)
.
p | The pointer argument. |
size | The size argument. |
ns | Namespace where the __CPROVER_havoc_slice symbol can be found. |
__CPROVER_havoc_slice
exists in the namespacenil_exprt() := __CPROVER_havoc_slice(p, size)
. Definition at line 78 of file goto_instruction_code.cpp.
|
inline |
Definition at line 117 of file goto_instruction_code.h.
|
inline |
Definition at line 110 of file goto_instruction_code.h.
|
inline |
Definition at line 187 of file goto_instruction_code.h.
|
inline |
Definition at line 180 of file goto_instruction_code.h.
|
inline |
Definition at line 252 of file goto_instruction_code.h.
|
inline |
Definition at line 245 of file goto_instruction_code.h.
|
inline |
Definition at line 384 of file goto_instruction_code.h.
|
inline |
Definition at line 377 of file goto_instruction_code.h.
|
inline |
Definition at line 534 of file goto_instruction_code.h.
|
inline |
Definition at line 527 of file goto_instruction_code.h.
|
inline |
Definition at line 105 of file goto_instruction_code.h.
|
inline |
Definition at line 175 of file goto_instruction_code.h.
|
inline |
Definition at line 240 of file goto_instruction_code.h.
|
inline |
Definition at line 372 of file goto_instruction_code.h.
|
inline |
Definition at line 433 of file goto_instruction_code.h.
|
inline |
Definition at line 479 of file goto_instruction_code.h.
|
inline |
Definition at line 522 of file goto_instruction_code.h.