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 1789 of file std_code.h.
|
inline |
Definition at line 1700 of file std_code.h.
|
inline |
Definition at line 613 of file std_code.h.
|
inline |
Definition at line 376 of file std_code.h.
|
inline |
Definition at line 561 of file std_code.h.
|
inline |
Definition at line 251 of file std_code.h.
|
inline |
Definition at line 1621 of file std_code.h.
|
inline |
Definition at line 1657 of file std_code.h.
|
inline |
Definition at line 512 of file std_code.h.
|
inline |
Definition at line 443 of file std_code.h.
|
inline |
Definition at line 995 of file std_code.h.
|
inline |
Definition at line 1844 of file std_code.h.
|
inline |
Definition at line 1102 of file std_code.h.
|
inline |
Definition at line 1287 of file std_code.h.
|
inline |
Definition at line 1576 of file std_code.h.
|
inline |
Definition at line 1154 of file std_code.h.
|
inline |
Definition at line 809 of file std_code.h.
|
inline |
Definition at line 676 of file std_code.h.
|
inline |
Definition at line 1420 of file std_code.h.
|
inline |
Definition at line 2417 of file std_code.h.
|
inline |
Definition at line 722 of file std_code.h.
|
inline |
Definition at line 2365 of file std_code.h.
|
inline |
Definition at line 2328 of file std_code.h.
|
inline |
Definition at line 1352 of file std_code.h.
|
inline |
Definition at line 286 of file std_code.h.
|
inline |
Definition at line 1493 of file std_code.h.
|
inline |
Definition at line 871 of file std_code.h.
|
inline |
Definition at line 2493 of file std_code.h.
|
inline |
Definition at line 933 of file std_code.h.
|
inline |
Definition at line 150 of file std_code.h.
|
inline |
Definition at line 2048 of file std_code.h.
|
inline |
Definition at line 2183 of file std_code.h.
|
inline |
Definition at line 1975 of file std_code.h.
|
inline |
Definition at line 2097 of file std_code.h.
|
inline |
Definition at line 2223 of file std_code.h.
|
inline |
Definition at line 1933 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 139 of file std_code.cpp.
Definition at line 158 of file std_code.h.
Definition at line 164 of file std_code.h.
Definition at line 1708 of file std_code.h.
Definition at line 1714 of file std_code.h.
|
inline |
Definition at line 1799 of file std_code.h.
|
inline |
Definition at line 1808 of file std_code.h.
|
inline |
Definition at line 631 of file std_code.h.
|
inline |
Definition at line 623 of file std_code.h.
|
inline |
Definition at line 393 of file std_code.h.
|
inline |
Definition at line 386 of file std_code.h.
|
inline |
Definition at line 579 of file std_code.h.
|
inline |
Definition at line 571 of file std_code.h.
|
inline |
Definition at line 265 of file std_code.h.
|
inline |
Definition at line 259 of file std_code.h.
|
inline |
Definition at line 1635 of file std_code.h.
|
inline |
Definition at line 1629 of file std_code.h.
|
inline |
Definition at line 1671 of file std_code.h.
|
inline |
Definition at line 1665 of file std_code.h.
|
inline |
Definition at line 529 of file std_code.h.
|
inline |
Definition at line 522 of file std_code.h.
|
inline |
Definition at line 460 of file std_code.h.
|
inline |
Definition at line 453 of file std_code.h.
|
inline |
Definition at line 1013 of file std_code.h.
|
inline |
Definition at line 1005 of file std_code.h.
|
inline |
Definition at line 1854 of file std_code.h.
|
inline |
Definition at line 1862 of file std_code.h.
Definition at line 1120 of file std_code.h.
Definition at line 1112 of file std_code.h.
|
inline |
Definition at line 2561 of file std_code.h.
|
inline |
Definition at line 2553 of file std_code.h.
|
inline |
Definition at line 1304 of file std_code.h.
|
inline |
Definition at line 1297 of file std_code.h.
|
inline |
Definition at line 1596 of file std_code.h.
|
inline |
Definition at line 1587 of file std_code.h.
|
inline |
Definition at line 1172 of file std_code.h.
|
inline |
Definition at line 1164 of file std_code.h.
|
inline |
Definition at line 827 of file std_code.h.
|
inline |
Definition at line 819 of file std_code.h.
|
inline |
Definition at line 1438 of file std_code.h.
|
inline |
Definition at line 1430 of file std_code.h.
|
inlinestatic |
Definition at line 2425 of file std_code.h.
|
inlinestatic |
Definition at line 2431 of file std_code.h.
|
inlinestatic |
Definition at line 2373 of file std_code.h.
|
inlinestatic |
Definition at line 2379 of file std_code.h.
|
inlinestatic |
Definition at line 2336 of file std_code.h.
|
inlinestatic |
Definition at line 2342 of file std_code.h.
|
inline |
Definition at line 1369 of file std_code.h.
|
inline |
Definition at line 1362 of file std_code.h.
|
inline |
Definition at line 889 of file std_code.h.
|
inline |
Definition at line 881 of file std_code.h.
|
inline |
Definition at line 1511 of file std_code.h.
|
inline |
Definition at line 1503 of file std_code.h.
|
inline |
Definition at line 2511 of file std_code.h.
|
inline |
Definition at line 2503 of file std_code.h.
|
inline |
Definition at line 951 of file std_code.h.
|
inline |
Definition at line 943 of file std_code.h.
|
inline |
Definition at line 1947 of file std_code.h.
|
inline |
Definition at line 1941 of file std_code.h.
|
inline |
Definition at line 2061 of file std_code.h.
|
inline |
Definition at line 2053 of file std_code.h.
|
inline |
Definition at line 2200 of file std_code.h.
|
inline |
Definition at line 2192 of file std_code.h.
|
inline |
Definition at line 1990 of file std_code.h.
|
inline |
Definition at line 1983 of file std_code.h.
|
inline |
Definition at line 2115 of file std_code.h.
|
inline |
Definition at line 2104 of file std_code.h.
|
inline |
Definition at line 2238 of file std_code.h.
|
inline |
Definition at line 2231 of file std_code.h.
|
inline |
Definition at line 1794 of file std_code.h.
|
inline |
Definition at line 618 of file std_code.h.
|
inline |
Definition at line 381 of file std_code.h.
|
inline |
Definition at line 566 of file std_code.h.
|
inline |
Definition at line 517 of file std_code.h.
|
inline |
Definition at line 448 of file std_code.h.
|
inline |
Definition at line 1000 of file std_code.h.
|
inline |
Definition at line 1849 of file std_code.h.
|
inline |
Definition at line 1107 of file std_code.h.
|
inline |
Definition at line 1292 of file std_code.h.
|
inline |
Definition at line 1581 of file std_code.h.
|
inline |
Definition at line 1159 of file std_code.h.
|
inline |
Definition at line 814 of file std_code.h.
|
inline |
Definition at line 681 of file std_code.h.
|
inline |
Definition at line 1425 of file std_code.h.
|
inline |
Definition at line 727 of file std_code.h.
|
inline |
Definition at line 1357 of file std_code.h.
|
inline |
Definition at line 1498 of file std_code.h.
|
inline |
Definition at line 876 of file std_code.h.
|
inline |
Definition at line 2498 of file std_code.h.
|
inline |
Definition at line 938 of file std_code.h.