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 1811 of file std_code.h.
|
inline |
Definition at line 1722 of file std_code.h.
|
inline |
Definition at line 642 of file std_code.h.
|
inline |
Definition at line 373 of file std_code.h.
|
inline |
Definition at line 590 of file std_code.h.
|
inline |
Definition at line 248 of file std_code.h.
|
inline |
Definition at line 1643 of file std_code.h.
|
inline |
Definition at line 1679 of file std_code.h.
|
inline |
Definition at line 541 of file std_code.h.
|
inline |
Definition at line 472 of file std_code.h.
|
inline |
Definition at line 1024 of file std_code.h.
|
inline |
Definition at line 1866 of file std_code.h.
|
inline |
Definition at line 1131 of file std_code.h.
|
inline |
Definition at line 1316 of file std_code.h.
|
inline |
Definition at line 1598 of file std_code.h.
|
inline |
Definition at line 1183 of file std_code.h.
|
inline |
Definition at line 838 of file std_code.h.
|
inline |
Definition at line 705 of file std_code.h.
|
inline |
Definition at line 1442 of file std_code.h.
|
inline |
Definition at line 2412 of file std_code.h.
|
inline |
Definition at line 751 of file std_code.h.
|
inline |
Definition at line 2360 of file std_code.h.
|
inline |
Definition at line 2323 of file std_code.h.
|
inline |
Definition at line 1381 of file std_code.h.
|
inline |
Definition at line 283 of file std_code.h.
|
inline |
Definition at line 1515 of file std_code.h.
|
inline |
Definition at line 900 of file std_code.h.
|
inline |
Definition at line 2488 of file std_code.h.
|
inline |
Definition at line 962 of file std_code.h.
|
inline |
Definition at line 147 of file std_code.h.
|
inline |
Definition at line 2061 of file std_code.h.
|
inline |
Definition at line 2178 of file std_code.h.
|
inline |
Definition at line 1988 of file std_code.h.
|
inline |
Definition at line 2110 of file std_code.h.
|
inline |
Definition at line 2218 of file std_code.h.
|
inline |
Definition at line 1946 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 122 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 1730 of file std_code.h.
Definition at line 1736 of file std_code.h.
|
inline |
Definition at line 1821 of file std_code.h.
|
inline |
Definition at line 1830 of file std_code.h.
|
inline |
Definition at line 660 of file std_code.h.
|
inline |
Definition at line 652 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 608 of file std_code.h.
|
inline |
Definition at line 600 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 1657 of file std_code.h.
|
inline |
Definition at line 1651 of file std_code.h.
|
inline |
Definition at line 1693 of file std_code.h.
|
inline |
Definition at line 1687 of file std_code.h.
|
inline |
Definition at line 558 of file std_code.h.
|
inline |
Definition at line 551 of file std_code.h.
|
inline |
Definition at line 489 of file std_code.h.
|
inline |
Definition at line 482 of file std_code.h.
|
inline |
Definition at line 1042 of file std_code.h.
|
inline |
Definition at line 1034 of file std_code.h.
|
inline |
Definition at line 1876 of file std_code.h.
|
inline |
Definition at line 1884 of file std_code.h.
Definition at line 1149 of file std_code.h.
Definition at line 1141 of file std_code.h.
|
inline |
Definition at line 2556 of file std_code.h.
|
inline |
Definition at line 2548 of file std_code.h.
|
inline |
Definition at line 1333 of file std_code.h.
|
inline |
Definition at line 1326 of file std_code.h.
|
inline |
Definition at line 1618 of file std_code.h.
|
inline |
Definition at line 1609 of file std_code.h.
|
inline |
Definition at line 1201 of file std_code.h.
|
inline |
Definition at line 1193 of file std_code.h.
|
inline |
Definition at line 856 of file std_code.h.
|
inline |
Definition at line 848 of file std_code.h.
|
inline |
Definition at line 1460 of file std_code.h.
|
inline |
Definition at line 1452 of file std_code.h.
|
inlinestatic |
Definition at line 2420 of file std_code.h.
|
inlinestatic |
Definition at line 2426 of file std_code.h.
|
inlinestatic |
Definition at line 2368 of file std_code.h.
|
inlinestatic |
Definition at line 2374 of file std_code.h.
|
inlinestatic |
Definition at line 2331 of file std_code.h.
|
inlinestatic |
Definition at line 2337 of file std_code.h.
|
inline |
Definition at line 1398 of file std_code.h.
|
inline |
Definition at line 1391 of file std_code.h.
|
inline |
Definition at line 918 of file std_code.h.
|
inline |
Definition at line 910 of file std_code.h.
|
inline |
Definition at line 1533 of file std_code.h.
|
inline |
Definition at line 1525 of file std_code.h.
|
inline |
Definition at line 2506 of file std_code.h.
|
inline |
Definition at line 2498 of file std_code.h.
|
inline |
Definition at line 980 of file std_code.h.
|
inline |
Definition at line 972 of file std_code.h.
|
inline |
Definition at line 1960 of file std_code.h.
|
inline |
Definition at line 1954 of file std_code.h.
|
inline |
Definition at line 2074 of file std_code.h.
|
inline |
Definition at line 2066 of file std_code.h.
|
inline |
Definition at line 2195 of file std_code.h.
|
inline |
Definition at line 2187 of file std_code.h.
|
inline |
Definition at line 2003 of file std_code.h.
|
inline |
Definition at line 1996 of file std_code.h.
|
inline |
Definition at line 2128 of file std_code.h.
|
inline |
Definition at line 2117 of file std_code.h.
|
inline |
Definition at line 2233 of file std_code.h.
|
inline |
Definition at line 2226 of file std_code.h.
|
inline |
Definition at line 1816 of file std_code.h.
|
inline |
Definition at line 647 of file std_code.h.
|
inline |
Definition at line 378 of file std_code.h.
|
inline |
Definition at line 595 of file std_code.h.
|
inline |
Definition at line 546 of file std_code.h.
|
inline |
Definition at line 477 of file std_code.h.
|
inline |
Definition at line 1029 of file std_code.h.
|
inline |
Definition at line 1871 of file std_code.h.
|
inline |
Definition at line 1136 of file std_code.h.
|
inline |
Definition at line 1321 of file std_code.h.
|
inline |
Definition at line 1603 of file std_code.h.
|
inline |
Definition at line 1188 of file std_code.h.
|
inline |
Definition at line 843 of file std_code.h.
|
inline |
Definition at line 710 of file std_code.h.
|
inline |
Definition at line 1447 of file std_code.h.
|
inline |
Definition at line 756 of file std_code.h.
|
inline |
Definition at line 1386 of file std_code.h.
|
inline |
Definition at line 1520 of file std_code.h.
|
inline |
Definition at line 905 of file std_code.h.
|
inline |
Definition at line 2493 of file std_code.h.
|
inline |
Definition at line 967 of file std_code.h.