cprover
|
#include <list>
#include "expr.h"
#include "expr_cast.h"
#include "invariant.h"
#include "std_expr.h"
#include "std_types.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 1779 of file std_code.h.
|
inline |
Definition at line 1690 of file std_code.h.
|
inline |
Definition at line 610 of file std_code.h.
|
inline |
Definition at line 373 of file std_code.h.
|
inline |
Definition at line 558 of file std_code.h.
|
inline |
Definition at line 248 of file std_code.h.
|
inline |
Definition at line 1611 of file std_code.h.
|
inline |
Definition at line 1647 of file std_code.h.
|
inline |
Definition at line 509 of file std_code.h.
|
inline |
Definition at line 440 of file std_code.h.
|
inline |
Definition at line 992 of file std_code.h.
|
inline |
Definition at line 1834 of file std_code.h.
|
inline |
Definition at line 1099 of file std_code.h.
|
inline |
Definition at line 1284 of file std_code.h.
|
inline |
Definition at line 1566 of file std_code.h.
|
inline |
Definition at line 1151 of file std_code.h.
|
inline |
Definition at line 806 of file std_code.h.
|
inline |
Definition at line 673 of file std_code.h.
|
inline |
Definition at line 1410 of file std_code.h.
|
inline |
Definition at line 2407 of file std_code.h.
|
inline |
Definition at line 719 of file std_code.h.
|
inline |
Definition at line 2355 of file std_code.h.
|
inline |
Definition at line 2318 of file std_code.h.
|
inline |
Definition at line 1349 of file std_code.h.
|
inline |
Definition at line 283 of file std_code.h.
|
inline |
Definition at line 1483 of file std_code.h.
|
inline |
Definition at line 868 of file std_code.h.
|
inline |
Definition at line 2483 of file std_code.h.
|
inline |
Definition at line 930 of file std_code.h.
|
inline |
Definition at line 147 of file std_code.h.
|
inline |
Definition at line 2038 of file std_code.h.
|
inline |
Definition at line 2173 of file std_code.h.
|
inline |
Definition at line 1965 of file std_code.h.
|
inline |
Definition at line 2087 of file std_code.h.
|
inline |
Definition at line 2213 of file std_code.h.
|
inline |
Definition at line 1923 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 121 of file std_code.cpp.
Definition at line 155 of file std_code.h.
Definition at line 161 of file std_code.h.
Definition at line 1698 of file std_code.h.
Definition at line 1704 of file std_code.h.
|
inline |
Definition at line 1789 of file std_code.h.
|
inline |
Definition at line 1798 of file std_code.h.
|
inline |
Definition at line 628 of file std_code.h.
|
inline |
Definition at line 620 of file std_code.h.
|
inline |
Definition at line 390 of file std_code.h.
|
inline |
Definition at line 383 of file std_code.h.
|
inline |
Definition at line 576 of file std_code.h.
|
inline |
Definition at line 568 of file std_code.h.
|
inline |
Definition at line 262 of file std_code.h.
|
inline |
Definition at line 256 of file std_code.h.
|
inline |
Definition at line 1625 of file std_code.h.
|
inline |
Definition at line 1619 of file std_code.h.
|
inline |
Definition at line 1661 of file std_code.h.
|
inline |
Definition at line 1655 of file std_code.h.
|
inline |
Definition at line 526 of file std_code.h.
|
inline |
Definition at line 519 of file std_code.h.
|
inline |
Definition at line 457 of file std_code.h.
|
inline |
Definition at line 450 of file std_code.h.
|
inline |
Definition at line 1010 of file std_code.h.
|
inline |
Definition at line 1002 of file std_code.h.
|
inline |
Definition at line 1844 of file std_code.h.
|
inline |
Definition at line 1852 of file std_code.h.
Definition at line 1117 of file std_code.h.
Definition at line 1109 of file std_code.h.
|
inline |
Definition at line 2551 of file std_code.h.
|
inline |
Definition at line 2543 of file std_code.h.
|
inline |
Definition at line 1301 of file std_code.h.
|
inline |
Definition at line 1294 of file std_code.h.
|
inline |
Definition at line 1586 of file std_code.h.
|
inline |
Definition at line 1577 of file std_code.h.
|
inline |
Definition at line 1169 of file std_code.h.
|
inline |
Definition at line 1161 of file std_code.h.
|
inline |
Definition at line 824 of file std_code.h.
|
inline |
Definition at line 816 of file std_code.h.
|
inline |
Definition at line 1428 of file std_code.h.
|
inline |
Definition at line 1420 of file std_code.h.
|
inlinestatic |
Definition at line 2415 of file std_code.h.
|
inlinestatic |
Definition at line 2421 of file std_code.h.
|
inlinestatic |
Definition at line 2363 of file std_code.h.
|
inlinestatic |
Definition at line 2369 of file std_code.h.
|
inlinestatic |
Definition at line 2326 of file std_code.h.
|
inlinestatic |
Definition at line 2332 of file std_code.h.
|
inline |
Definition at line 1366 of file std_code.h.
|
inline |
Definition at line 1359 of file std_code.h.
|
inline |
Definition at line 886 of file std_code.h.
|
inline |
Definition at line 878 of file std_code.h.
|
inline |
Definition at line 1501 of file std_code.h.
|
inline |
Definition at line 1493 of file std_code.h.
|
inline |
Definition at line 2501 of file std_code.h.
|
inline |
Definition at line 2493 of file std_code.h.
|
inline |
Definition at line 948 of file std_code.h.
|
inline |
Definition at line 940 of file std_code.h.
|
inline |
Definition at line 1937 of file std_code.h.
|
inline |
Definition at line 1931 of file std_code.h.
|
inline |
Definition at line 2051 of file std_code.h.
|
inline |
Definition at line 2043 of file std_code.h.
|
inline |
Definition at line 2190 of file std_code.h.
|
inline |
Definition at line 2182 of file std_code.h.
|
inline |
Definition at line 1980 of file std_code.h.
|
inline |
Definition at line 1973 of file std_code.h.
|
inline |
Definition at line 2105 of file std_code.h.
|
inline |
Definition at line 2094 of file std_code.h.
|
inline |
Definition at line 2228 of file std_code.h.
|
inline |
Definition at line 2221 of file std_code.h.
|
inline |
Definition at line 1784 of file std_code.h.
|
inline |
Definition at line 615 of file std_code.h.
|
inline |
Definition at line 378 of file std_code.h.
|
inline |
Definition at line 563 of file std_code.h.
|
inline |
Definition at line 514 of file std_code.h.
|
inline |
Definition at line 445 of file std_code.h.
|
inline |
Definition at line 997 of file std_code.h.
|
inline |
Definition at line 1839 of file std_code.h.
|
inline |
Definition at line 1104 of file std_code.h.
|
inline |
Definition at line 1289 of file std_code.h.
|
inline |
Definition at line 1571 of file std_code.h.
|
inline |
Definition at line 1156 of file std_code.h.
|
inline |
Definition at line 811 of file std_code.h.
|
inline |
Definition at line 678 of file std_code.h.
|
inline |
Definition at line 1415 of file std_code.h.
|
inline |
Definition at line 724 of file std_code.h.
|
inline |
Definition at line 1354 of file std_code.h.
|
inline |
Definition at line 1488 of file std_code.h.
|
inline |
Definition at line 873 of file std_code.h.
|
inline |
Definition at line 2488 of file std_code.h.
|
inline |
Definition at line 935 of file std_code.h.