cprover
|
#include <list>
#include "expr_cast.h"
#include "invariant.h"
#include "std_expr.h"
#include "validate.h"
#include "validate_code.h"
Go to the source code of this file.
Classes | |
class | codet |
Data structure for representing an arbitrary statement in a program. More... | |
class | code_blockt |
A codet representing sequential composition of program statements. More... | |
class | code_skipt |
A codet representing a skip statement. More... | |
class | code_assignt |
A codet representing an assignment in the program. More... | |
class | code_declt |
A codet representing the declaration of a local variable. More... | |
class | code_deadt |
A codet representing the removal of a local variable going out of scope. More... | |
class | code_assumet |
An assumption, which must hold in subsequent code. More... | |
class | code_assertt |
A non-fatal assertion, which checks a condition then permits execution to continue. 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_ifthenelset |
codet representation of an if-then-else statement. More... | |
class | code_switcht |
codet representing a switch statement. More... | |
class | code_whilet |
codet representing a while statement. More... | |
class | code_dowhilet |
codet representation of a do while statement. More... | |
class | code_fort |
codet representation of a for statement. More... | |
class | code_gotot |
codet representation of a goto statement. More... | |
class | code_function_callt |
codet representation of a function call statement. More... | |
class | code_returnt |
codet representation of a "return from a function" statement. More... | |
class | code_labelt |
codet representation of a label for branch targets. More... | |
class | code_switch_caset |
codet representation of a switch-case, i.e. a case statement within a switch . More... | |
class | code_gcc_switch_case_ranget |
codet representation of a switch-case, i.e. a case statement within a switch . More... | |
class | code_breakt |
codet representation of a break statement (within a for or while loop). More... | |
class | code_continuet |
codet representation of a continue statement (within a for or while loop). More... | |
class | code_asmt |
codet representation of an inline assembler statement. More... | |
class | code_asm_gcct |
codet representation of an inline assembler statement, for the gcc flavor. More... | |
class | code_expressiont |
codet representation of an expression statement. More... | |
class | side_effect_exprt |
An expression containing a side effect. More... | |
class | side_effect_expr_nondett |
A side_effect_exprt that returns a non-deterministically chosen value. More... | |
class | side_effect_expr_assignt |
A side_effect_exprt that performs an assignment. More... | |
class | side_effect_expr_statement_expressiont |
A side_effect_exprt that contains a statement. More... | |
class | side_effect_expr_function_callt |
A side_effect_exprt representation of a function call side effect. More... | |
class | side_effect_expr_throwt |
A side_effect_exprt representation of a side effect that throws an exception. More... | |
class | code_push_catcht |
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ... More... | |
class | code_push_catcht::exception_list_entryt |
class | code_pop_catcht |
Pops an exception handler from the stack of active handlers (i.e. More... | |
class | code_landingpadt |
A statement that catches an exception, assigning the exception in flight to an expression (e.g. More... | |
class | code_try_catcht |
codet representation of a try/catch block. More... | |
class | code_function_bodyt |
This class is used to interface between a language frontend and goto-convert – it communicates the identifiers of the parameters of a function or method. More... | |
Namespaces | |
detail | |
|
inline |
Definition at line 1809 of file std_code.h.
|
inline |
Definition at line 1720 of file std_code.h.
|
inline |
Definition at line 640 of file std_code.h.
|
inline |
Definition at line 371 of file std_code.h.
|
inline |
Definition at line 588 of file std_code.h.
|
inline |
Definition at line 246 of file std_code.h.
|
inline |
Definition at line 1641 of file std_code.h.
|
inline |
Definition at line 1677 of file std_code.h.
|
inline |
Definition at line 539 of file std_code.h.
|
inline |
Definition at line 470 of file std_code.h.
|
inline |
Definition at line 1022 of file std_code.h.
|
inline |
Definition at line 1864 of file std_code.h.
|
inline |
Definition at line 1129 of file std_code.h.
|
inline |
Definition at line 1314 of file std_code.h.
|
inline |
Definition at line 1596 of file std_code.h.
|
inline |
Definition at line 1181 of file std_code.h.
|
inline |
Definition at line 836 of file std_code.h.
|
inline |
Definition at line 703 of file std_code.h.
|
inline |
Definition at line 1440 of file std_code.h.
|
inline |
Definition at line 2410 of file std_code.h.
|
inline |
Definition at line 749 of file std_code.h.
|
inline |
Definition at line 2358 of file std_code.h.
|
inline |
Definition at line 2321 of file std_code.h.
|
inline |
Definition at line 1379 of file std_code.h.
|
inline |
Definition at line 281 of file std_code.h.
|
inline |
Definition at line 1513 of file std_code.h.
|
inline |
Definition at line 898 of file std_code.h.
|
inline |
Definition at line 2486 of file std_code.h.
|
inline |
Definition at line 960 of file std_code.h.
|
inline |
Definition at line 145 of file std_code.h.
|
inline |
Definition at line 2059 of file std_code.h.
|
inline |
Definition at line 2176 of file std_code.h.
|
inline |
Definition at line 1986 of file std_code.h.
|
inline |
Definition at line 2108 of file std_code.h.
|
inline |
Definition at line 2216 of file std_code.h.
|
inline |
Definition at line 1944 of file std_code.h.
code_blockt create_fatal_assertion | ( | const exprt & | condition, |
const source_locationt & | source_location | ||
) |
Create a fatal assertion, which checks a condition and then halts if it does not hold.
Equivalent to ASSERT(condition); ASSUME(condition)
.
Source level assertions should probably use this, whilst checks that are normally non-fatal at runtime, such as integer overflows, should use code_assertt by itself.
condition | condition to assert |
source_location | source location to attach to the generated code; conventionally this should have comment and property_class fields set to indicate the nature of the assertion. |
Definition at line 123 of file std_code.cpp.
Definition at line 153 of file std_code.h.
Definition at line 159 of file std_code.h.
Definition at line 1728 of file std_code.h.
Definition at line 1734 of file std_code.h.
|
inline |
Definition at line 1819 of file std_code.h.
|
inline |
Definition at line 1828 of file std_code.h.
|
inline |
Definition at line 658 of file std_code.h.
|
inline |
Definition at line 650 of file std_code.h.
|
inline |
Definition at line 388 of file std_code.h.
|
inline |
Definition at line 381 of file std_code.h.
|
inline |
Definition at line 606 of file std_code.h.
|
inline |
Definition at line 598 of file std_code.h.
|
inline |
Definition at line 260 of file std_code.h.
|
inline |
Definition at line 254 of file std_code.h.
|
inline |
Definition at line 1655 of file std_code.h.
|
inline |
Definition at line 1649 of file std_code.h.
|
inline |
Definition at line 1691 of file std_code.h.
|
inline |
Definition at line 1685 of file std_code.h.
|
inline |
Definition at line 556 of file std_code.h.
|
inline |
Definition at line 549 of file std_code.h.
|
inline |
Definition at line 487 of file std_code.h.
|
inline |
Definition at line 480 of file std_code.h.
|
inline |
Definition at line 1040 of file std_code.h.
|
inline |
Definition at line 1032 of file std_code.h.
|
inline |
Definition at line 1874 of file std_code.h.
|
inline |
Definition at line 1882 of file std_code.h.
Definition at line 1147 of file std_code.h.
Definition at line 1139 of file std_code.h.
|
inline |
Definition at line 2554 of file std_code.h.
|
inline |
Definition at line 2546 of file std_code.h.
|
inline |
Definition at line 1331 of file std_code.h.
|
inline |
Definition at line 1324 of file std_code.h.
|
inline |
Definition at line 1616 of file std_code.h.
|
inline |
Definition at line 1607 of file std_code.h.
|
inline |
Definition at line 1199 of file std_code.h.
|
inline |
Definition at line 1191 of file std_code.h.
|
inline |
Definition at line 854 of file std_code.h.
|
inline |
Definition at line 846 of file std_code.h.
|
inline |
Definition at line 1458 of file std_code.h.
|
inline |
Definition at line 1450 of file std_code.h.
|
inlinestatic |
Definition at line 2418 of file std_code.h.
|
inlinestatic |
Definition at line 2424 of file std_code.h.
|
inlinestatic |
Definition at line 2366 of file std_code.h.
|
inlinestatic |
Definition at line 2372 of file std_code.h.
|
inlinestatic |
Definition at line 2329 of file std_code.h.
|
inlinestatic |
Definition at line 2335 of file std_code.h.
|
inline |
Definition at line 1396 of file std_code.h.
|
inline |
Definition at line 1389 of file std_code.h.
|
inline |
Definition at line 916 of file std_code.h.
|
inline |
Definition at line 908 of file std_code.h.
|
inline |
Definition at line 1531 of file std_code.h.
|
inline |
Definition at line 1523 of file std_code.h.
|
inline |
Definition at line 2504 of file std_code.h.
|
inline |
Definition at line 2496 of file std_code.h.
|
inline |
Definition at line 978 of file std_code.h.
|
inline |
Definition at line 970 of file std_code.h.
|
inline |
Definition at line 1958 of file std_code.h.
|
inline |
Definition at line 1952 of file std_code.h.
|
inline |
Definition at line 2072 of file std_code.h.
|
inline |
Definition at line 2064 of file std_code.h.
|
inline |
Definition at line 2193 of file std_code.h.
|
inline |
Definition at line 2185 of file std_code.h.
|
inline |
Definition at line 2001 of file std_code.h.
|
inline |
Definition at line 1994 of file std_code.h.
|
inline |
Definition at line 2126 of file std_code.h.
|
inline |
Definition at line 2115 of file std_code.h.
|
inline |
Definition at line 2231 of file std_code.h.
|
inline |
Definition at line 2224 of file std_code.h.
|
inline |
Definition at line 1814 of file std_code.h.
|
inline |
Definition at line 645 of file std_code.h.
|
inline |
Definition at line 376 of file std_code.h.
|
inline |
Definition at line 593 of file std_code.h.
|
inline |
Definition at line 544 of file std_code.h.
|
inline |
Definition at line 475 of file std_code.h.
|
inline |
Definition at line 1027 of file std_code.h.
|
inline |
Definition at line 1869 of file std_code.h.
|
inline |
Definition at line 1134 of file std_code.h.
|
inline |
Definition at line 1319 of file std_code.h.
|
inline |
Definition at line 1601 of file std_code.h.
|
inline |
Definition at line 1186 of file std_code.h.
|
inline |
Definition at line 841 of file std_code.h.
|
inline |
Definition at line 708 of file std_code.h.
|
inline |
Definition at line 1445 of file std_code.h.
|
inline |
Definition at line 754 of file std_code.h.
|
inline |
Definition at line 1384 of file std_code.h.
|
inline |
Definition at line 1518 of file std_code.h.
|
inline |
Definition at line 903 of file std_code.h.
|
inline |
Definition at line 2491 of file std_code.h.
|
inline |
Definition at line 965 of file std_code.h.