cprover
|
#include <list>
#include "base_type.h"
#include "expr.h"
#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_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_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_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_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... | |
Namespaces | |
detail | |
|
inline |
Definition at line 1482 of file std_code.h.
|
inline |
Definition at line 573 of file std_code.h.
|
inline |
Definition at line 324 of file std_code.h.
|
inline |
Definition at line 521 of file std_code.h.
|
inline |
Definition at line 216 of file std_code.h.
|
inline |
Definition at line 1408 of file std_code.h.
|
inline |
Definition at line 1438 of file std_code.h.
|
inline |
Definition at line 463 of file std_code.h.
|
inline |
Definition at line 389 of file std_code.h.
|
inline |
Definition at line 866 of file std_code.h.
|
inline |
Definition at line 1529 of file std_code.h.
|
inline |
Definition at line 958 of file std_code.h.
|
inline |
Definition at line 1165 of file std_code.h.
|
inline |
Definition at line 1007 of file std_code.h.
|
inline |
Definition at line 678 of file std_code.h.
|
inline |
Definition at line 1300 of file std_code.h.
|
inline |
Definition at line 1986 of file std_code.h.
|
inline |
Definition at line 1941 of file std_code.h.
|
inline |
Definition at line 1910 of file std_code.h.
|
inline |
Definition at line 1230 of file std_code.h.
|
inline |
Definition at line 245 of file std_code.h.
|
inline |
Definition at line 1372 of file std_code.h.
|
inline |
Definition at line 742 of file std_code.h.
|
inline |
Definition at line 2062 of file std_code.h.
|
inline |
Definition at line 804 of file std_code.h.
|
inline |
Definition at line 128 of file std_code.h.
|
inline |
Definition at line 1766 of file std_code.h.
|
inline |
Definition at line 1667 of file std_code.h.
|
inline |
Definition at line 1811 of file std_code.h.
|
inline |
Definition at line 1612 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 136 of file std_code.cpp.
Definition at line 136 of file std_code.h.
Definition at line 142 of file std_code.h.
Definition at line 1490 of file std_code.h.
Definition at line 1496 of file std_code.h.
|
inline |
Definition at line 587 of file std_code.h.
|
inline |
Definition at line 581 of file std_code.h.
|
inline |
Definition at line 341 of file std_code.h.
|
inline |
Definition at line 334 of file std_code.h.
|
inline |
Definition at line 535 of file std_code.h.
|
inline |
Definition at line 529 of file std_code.h.
|
inline |
Definition at line 230 of file std_code.h.
|
inline |
Definition at line 224 of file std_code.h.
|
inline |
Definition at line 1422 of file std_code.h.
|
inline |
Definition at line 1416 of file std_code.h.
|
inline |
Definition at line 1452 of file std_code.h.
|
inline |
Definition at line 1446 of file std_code.h.
|
inline |
Definition at line 484 of file std_code.h.
|
inline |
Definition at line 473 of file std_code.h.
|
inline |
Definition at line 412 of file std_code.h.
|
inline |
Definition at line 399 of file std_code.h.
|
inline |
Definition at line 884 of file std_code.h.
|
inline |
Definition at line 876 of file std_code.h.
|
inline |
Definition at line 1539 of file std_code.h.
|
inline |
Definition at line 1547 of file std_code.h.
Definition at line 975 of file std_code.h.
Definition at line 968 of file std_code.h.
|
inline |
Definition at line 1179 of file std_code.h.
|
inline |
Definition at line 1173 of file std_code.h.
|
inline |
Definition at line 1024 of file std_code.h.
|
inline |
Definition at line 1017 of file std_code.h.
|
inline |
Definition at line 696 of file std_code.h.
|
inline |
Definition at line 688 of file std_code.h.
|
inline |
Definition at line 1317 of file std_code.h.
|
inline |
Definition at line 1310 of file std_code.h.
|
inlinestatic |
Definition at line 1994 of file std_code.h.
|
inlinestatic |
Definition at line 2000 of file std_code.h.
|
inlinestatic |
Definition at line 1949 of file std_code.h.
|
inlinestatic |
Definition at line 1955 of file std_code.h.
|
inlinestatic |
Definition at line 1918 of file std_code.h.
|
inlinestatic |
Definition at line 1924 of file std_code.h.
|
inline |
Definition at line 1244 of file std_code.h.
|
inline |
Definition at line 1238 of file std_code.h.
|
inline |
Definition at line 759 of file std_code.h.
|
inline |
Definition at line 752 of file std_code.h.
|
inline |
Definition at line 1390 of file std_code.h.
|
inline |
Definition at line 1382 of file std_code.h.
|
inline |
Definition at line 2080 of file std_code.h.
|
inline |
Definition at line 2072 of file std_code.h.
|
inline |
Definition at line 821 of file std_code.h.
|
inline |
Definition at line 814 of file std_code.h.
|
inline |
Definition at line 1626 of file std_code.h.
|
inline |
Definition at line 1620 of file std_code.h.
|
inline |
Definition at line 1783 of file std_code.h.
|
inline |
Definition at line 1775 of file std_code.h.
|
inline |
Definition at line 1682 of file std_code.h.
|
inline |
Definition at line 1675 of file std_code.h.
|
inline |
Definition at line 1826 of file std_code.h.
|
inline |
Definition at line 1819 of file std_code.h.
|
inline |
Definition at line 593 of file std_code.h.
|
inline |
Definition at line 329 of file std_code.h.
|
inline |
Definition at line 541 of file std_code.h.
|
inline |
Definition at line 468 of file std_code.h.
|
inline |
Definition at line 394 of file std_code.h.
|
inline |
Definition at line 871 of file std_code.h.
|
inline |
Definition at line 1534 of file std_code.h.
|
inline |
Definition at line 963 of file std_code.h.
|
inline |
Definition at line 1185 of file std_code.h.
|
inline |
Definition at line 1012 of file std_code.h.
|
inline |
Definition at line 683 of file std_code.h.
|
inline |
Definition at line 1305 of file std_code.h.
|
inline |
Definition at line 1250 of file std_code.h.
|
inline |
Definition at line 1377 of file std_code.h.
|
inline |
Definition at line 747 of file std_code.h.
|
inline |
Definition at line 2067 of file std_code.h.
|
inline |
Definition at line 809 of file std_code.h.