cprover
std_code.h File Reference
#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"
+ Include dependency graph for std_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_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
 

Functions

template<typename Tag >
bool detail::can_cast_code_impl (const exprt &expr, const Tag &tag)
 
template<>
bool can_cast_expr< codet > (const exprt &base)
 
const codetto_code (const exprt &expr)
 
codetto_code (exprt &expr)
 
template<>
bool can_cast_expr< code_blockt > (const exprt &base)
 
const code_blocktto_code_block (const codet &code)
 
code_blocktto_code_block (codet &code)
 
template<>
bool can_cast_expr< code_skipt > (const exprt &base)
 
template<>
bool can_cast_expr< code_assignt > (const exprt &base)
 
void validate_expr (const code_assignt &x)
 
const code_assigntto_code_assign (const codet &code)
 
code_assigntto_code_assign (codet &code)
 
template<>
bool can_cast_expr< code_declt > (const exprt &base)
 
void validate_expr (const code_declt &x)
 
const code_decltto_code_decl (const codet &code)
 
code_decltto_code_decl (codet &code)
 
template<>
bool can_cast_expr< code_deadt > (const exprt &base)
 
void validate_expr (const code_deadt &x)
 
const code_deadtto_code_dead (const codet &code)
 
code_deadtto_code_dead (codet &code)
 
template<>
bool can_cast_expr< code_assumet > (const exprt &base)
 
void validate_expr (const code_assumet &x)
 
const code_assumetto_code_assume (const codet &code)
 
code_assumetto_code_assume (codet &code)
 
template<>
bool can_cast_expr< code_assertt > (const exprt &base)
 
void validate_expr (const code_assertt &x)
 
const code_asserttto_code_assert (const codet &code)
 
code_asserttto_code_assert (codet &code)
 
template<>
bool can_cast_expr< code_inputt > (const exprt &base)
 
void validate_expr (const code_inputt &input)
 
template<>
bool can_cast_expr< code_outputt > (const exprt &base)
 
void validate_expr (const code_outputt &output)
 
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. More...
 
template<>
bool can_cast_expr< code_ifthenelset > (const exprt &base)
 
void validate_expr (const code_ifthenelset &x)
 
const code_ifthenelsetto_code_ifthenelse (const codet &code)
 
code_ifthenelsetto_code_ifthenelse (codet &code)
 
template<>
bool can_cast_expr< code_switcht > (const exprt &base)
 
void validate_expr (const code_switcht &x)
 
const code_switchtto_code_switch (const codet &code)
 
code_switchtto_code_switch (codet &code)
 
template<>
bool can_cast_expr< code_whilet > (const exprt &base)
 
void validate_expr (const code_whilet &x)
 
const code_whiletto_code_while (const codet &code)
 
code_whiletto_code_while (codet &code)
 
template<>
bool can_cast_expr< code_dowhilet > (const exprt &base)
 
void validate_expr (const code_dowhilet &x)
 
const code_dowhiletto_code_dowhile (const codet &code)
 
code_dowhiletto_code_dowhile (codet &code)
 
template<>
bool can_cast_expr< code_fort > (const exprt &base)
 
void validate_expr (const code_fort &x)
 
const code_fortto_code_for (const codet &code)
 
code_fortto_code_for (codet &code)
 
template<>
bool can_cast_expr< code_gotot > (const exprt &base)
 
void validate_expr (const code_gotot &x)
 
const code_gototto_code_goto (const codet &code)
 
code_gototto_code_goto (codet &code)
 
template<>
bool can_cast_expr< code_function_callt > (const exprt &base)
 
void validate_expr (const code_function_callt &x)
 
const code_function_calltto_code_function_call (const codet &code)
 
code_function_calltto_code_function_call (codet &code)
 
template<>
bool can_cast_expr< code_returnt > (const exprt &base)
 
void validate_expr (const code_returnt &x)
 
const code_returntto_code_return (const codet &code)
 
code_returntto_code_return (codet &code)
 
template<>
bool can_cast_expr< code_labelt > (const exprt &base)
 
void validate_expr (const code_labelt &x)
 
const code_labeltto_code_label (const codet &code)
 
code_labeltto_code_label (codet &code)
 
template<>
bool can_cast_expr< code_switch_caset > (const exprt &base)
 
void validate_expr (const code_switch_caset &x)
 
const code_switch_casetto_code_switch_case (const codet &code)
 
code_switch_casetto_code_switch_case (codet &code)
 
template<>
bool can_cast_expr< code_gcc_switch_case_ranget > (const exprt &base)
 
void validate_expr (const code_gcc_switch_case_ranget &x)
 
const code_gcc_switch_case_rangetto_code_gcc_switch_case_range (const codet &code)
 
code_gcc_switch_case_rangetto_code_gcc_switch_case_range (codet &code)
 
template<>
bool can_cast_expr< code_breakt > (const exprt &base)
 
const code_breaktto_code_break (const codet &code)
 
code_breaktto_code_break (codet &code)
 
template<>
bool can_cast_expr< code_continuet > (const exprt &base)
 
const code_continuetto_code_continue (const codet &code)
 
code_continuetto_code_continue (codet &code)
 
template<>
bool can_cast_expr< code_asmt > (const exprt &base)
 
code_asmtto_code_asm (codet &code)
 
const code_asmtto_code_asm (const codet &code)
 
template<>
bool can_cast_expr< code_asm_gcct > (const exprt &base)
 
void validate_expr (const code_asm_gcct &x)
 
code_asm_gcctto_code_asm_gcc (codet &code)
 
const code_asm_gcctto_code_asm_gcc (const codet &code)
 
template<>
bool can_cast_expr< code_expressiont > (const exprt &base)
 
void validate_expr (const code_expressiont &x)
 
code_expressiontto_code_expression (codet &code)
 
const code_expressiontto_code_expression (const codet &code)
 
template<typename Tag >
bool detail::can_cast_side_effect_expr_impl (const exprt &expr, const Tag &tag)
 
template<>
bool can_cast_expr< side_effect_exprt > (const exprt &base)
 
side_effect_exprtto_side_effect_expr (exprt &expr)
 
const side_effect_exprtto_side_effect_expr (const exprt &expr)
 
template<>
bool can_cast_expr< side_effect_expr_nondett > (const exprt &base)
 
side_effect_expr_nondettto_side_effect_expr_nondet (exprt &expr)
 
const side_effect_expr_nondettto_side_effect_expr_nondet (const exprt &expr)
 
template<>
bool can_cast_expr< side_effect_expr_assignt > (const exprt &base)
 
side_effect_expr_assigntto_side_effect_expr_assign (exprt &expr)
 
const side_effect_expr_assigntto_side_effect_expr_assign (const exprt &expr)
 
template<>
bool can_cast_expr< side_effect_expr_function_callt > (const exprt &base)
 
side_effect_expr_function_calltto_side_effect_expr_function_call (exprt &expr)
 
const side_effect_expr_function_calltto_side_effect_expr_function_call (const exprt &expr)
 
template<>
bool can_cast_expr< side_effect_expr_throwt > (const exprt &base)
 
side_effect_expr_throwtto_side_effect_expr_throw (exprt &expr)
 
const side_effect_expr_throwtto_side_effect_expr_throw (const exprt &expr)
 
template<>
bool can_cast_expr< code_push_catcht > (const exprt &base)
 
static code_push_catchtto_code_push_catch (codet &code)
 
static const code_push_catchtto_code_push_catch (const codet &code)
 
template<>
bool can_cast_expr< code_pop_catcht > (const exprt &base)
 
static code_pop_catchtto_code_pop_catch (codet &code)
 
static const code_pop_catchtto_code_pop_catch (const codet &code)
 
template<>
bool can_cast_expr< code_landingpadt > (const exprt &base)
 
static code_landingpadtto_code_landingpad (codet &code)
 
static const code_landingpadtto_code_landingpad (const codet &code)
 
template<>
bool can_cast_expr< code_try_catcht > (const exprt &base)
 
void validate_expr (const code_try_catcht &x)
 
const code_try_catchtto_code_try_catch (const codet &code)
 
code_try_catchtto_code_try_catch (codet &code)
 
const code_function_bodytto_code_function_body (const codet &code)
 
code_function_bodytto_code_function_body (codet &code)
 

Function Documentation

◆ can_cast_expr< code_asm_gcct >()

template<>
bool can_cast_expr< code_asm_gcct > ( const exprt base)
inline

Definition at line 1786 of file std_code.h.

◆ can_cast_expr< code_asmt >()

template<>
bool can_cast_expr< code_asmt > ( const exprt base)
inline

Definition at line 1697 of file std_code.h.

◆ can_cast_expr< code_assertt >()

template<>
bool can_cast_expr< code_assertt > ( const exprt base)
inline

Definition at line 608 of file std_code.h.

◆ can_cast_expr< code_assignt >()

template<>
bool can_cast_expr< code_assignt > ( const exprt base)
inline

Definition at line 371 of file std_code.h.

◆ can_cast_expr< code_assumet >()

template<>
bool can_cast_expr< code_assumet > ( const exprt base)
inline

Definition at line 556 of file std_code.h.

◆ can_cast_expr< code_blockt >()

template<>
bool can_cast_expr< code_blockt > ( const exprt base)
inline

Definition at line 246 of file std_code.h.

◆ can_cast_expr< code_breakt >()

template<>
bool can_cast_expr< code_breakt > ( const exprt base)
inline

Definition at line 1618 of file std_code.h.

◆ can_cast_expr< code_continuet >()

template<>
bool can_cast_expr< code_continuet > ( const exprt base)
inline

Definition at line 1654 of file std_code.h.

◆ can_cast_expr< code_deadt >()

template<>
bool can_cast_expr< code_deadt > ( const exprt base)
inline

Definition at line 507 of file std_code.h.

◆ can_cast_expr< code_declt >()

template<>
bool can_cast_expr< code_declt > ( const exprt base)
inline

Definition at line 438 of file std_code.h.

◆ can_cast_expr< code_dowhilet >()

template<>
bool can_cast_expr< code_dowhilet > ( const exprt base)
inline

Definition at line 1002 of file std_code.h.

◆ can_cast_expr< code_expressiont >()

template<>
bool can_cast_expr< code_expressiont > ( const exprt base)
inline

Definition at line 1841 of file std_code.h.

◆ can_cast_expr< code_fort >()

template<>
bool can_cast_expr< code_fort > ( const exprt base)
inline

Definition at line 1099 of file std_code.h.

◆ can_cast_expr< code_function_callt >()

template<>
bool can_cast_expr< code_function_callt > ( const exprt base)
inline

Definition at line 1284 of file std_code.h.

◆ can_cast_expr< code_gcc_switch_case_ranget >()

template<>
bool can_cast_expr< code_gcc_switch_case_ranget > ( const exprt base)
inline

Definition at line 1573 of file std_code.h.

◆ can_cast_expr< code_gotot >()

template<>
bool can_cast_expr< code_gotot > ( const exprt base)
inline

Definition at line 1151 of file std_code.h.

◆ can_cast_expr< code_ifthenelset >()

template<>
bool can_cast_expr< code_ifthenelset > ( const exprt base)
inline

Definition at line 816 of file std_code.h.

◆ can_cast_expr< code_inputt >()

template<>
bool can_cast_expr< code_inputt > ( const exprt base)
inline

Definition at line 671 of file std_code.h.

◆ can_cast_expr< code_labelt >()

template<>
bool can_cast_expr< code_labelt > ( const exprt base)
inline

Definition at line 1417 of file std_code.h.

◆ can_cast_expr< code_landingpadt >()

template<>
bool can_cast_expr< code_landingpadt > ( const exprt base)
inline

Definition at line 2368 of file std_code.h.

◆ can_cast_expr< code_outputt >()

template<>
bool can_cast_expr< code_outputt > ( const exprt base)
inline

Definition at line 717 of file std_code.h.

◆ can_cast_expr< code_pop_catcht >()

template<>
bool can_cast_expr< code_pop_catcht > ( const exprt base)
inline

Definition at line 2316 of file std_code.h.

◆ can_cast_expr< code_push_catcht >()

template<>
bool can_cast_expr< code_push_catcht > ( const exprt base)
inline

Definition at line 2279 of file std_code.h.

◆ can_cast_expr< code_returnt >()

template<>
bool can_cast_expr< code_returnt > ( const exprt base)
inline

Definition at line 1349 of file std_code.h.

◆ can_cast_expr< code_skipt >()

template<>
bool can_cast_expr< code_skipt > ( const exprt base)
inline

Definition at line 281 of file std_code.h.

◆ can_cast_expr< code_switch_caset >()

template<>
bool can_cast_expr< code_switch_caset > ( const exprt base)
inline

Definition at line 1490 of file std_code.h.

◆ can_cast_expr< code_switcht >()

template<>
bool can_cast_expr< code_switcht > ( const exprt base)
inline

Definition at line 878 of file std_code.h.

◆ can_cast_expr< code_try_catcht >()

template<>
bool can_cast_expr< code_try_catcht > ( const exprt base)
inline

Definition at line 2450 of file std_code.h.

◆ can_cast_expr< code_whilet >()

template<>
bool can_cast_expr< code_whilet > ( const exprt base)
inline

Definition at line 940 of file std_code.h.

◆ can_cast_expr< codet >()

template<>
bool can_cast_expr< codet > ( const exprt base)
inline

Definition at line 145 of file std_code.h.

◆ can_cast_expr< side_effect_expr_assignt >()

template<>
bool can_cast_expr< side_effect_expr_assignt > ( const exprt base)
inline

Definition at line 2056 of file std_code.h.

◆ can_cast_expr< side_effect_expr_function_callt >()

template<>
bool can_cast_expr< side_effect_expr_function_callt > ( const exprt base)
inline

Definition at line 2134 of file std_code.h.

◆ can_cast_expr< side_effect_expr_nondett >()

template<>
bool can_cast_expr< side_effect_expr_nondett > ( const exprt base)
inline

Definition at line 1983 of file std_code.h.

◆ can_cast_expr< side_effect_expr_throwt >()

template<>
bool can_cast_expr< side_effect_expr_throwt > ( const exprt base)
inline

Definition at line 2174 of file std_code.h.

◆ can_cast_expr< side_effect_exprt >()

template<>
bool can_cast_expr< side_effect_exprt > ( const exprt base)
inline

Definition at line 1930 of file std_code.h.

◆ create_fatal_assertion()

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.

Parameters
conditioncondition to assert
source_locationsource location to attach to the generated code; conventionally this should have comment and property_class fields set to indicate the nature of the assertion.
Returns
A code block that asserts a condition then aborts if it does not hold.

Definition at line 139 of file std_code.cpp.

◆ to_code() [1/2]

const codet& to_code ( const exprt expr)
inline

Definition at line 153 of file std_code.h.

◆ to_code() [2/2]

codet& to_code ( exprt expr)
inline

Definition at line 159 of file std_code.h.

◆ to_code_asm() [1/2]

code_asmt& to_code_asm ( codet code)
inline

Definition at line 1705 of file std_code.h.

◆ to_code_asm() [2/2]

const code_asmt& to_code_asm ( const codet code)
inline

Definition at line 1711 of file std_code.h.

◆ to_code_asm_gcc() [1/2]

code_asm_gcct& to_code_asm_gcc ( codet code)
inline

Definition at line 1796 of file std_code.h.

◆ to_code_asm_gcc() [2/2]

const code_asm_gcct& to_code_asm_gcc ( const codet code)
inline

Definition at line 1805 of file std_code.h.

◆ to_code_assert() [1/2]

const code_assertt& to_code_assert ( const codet code)
inline

Definition at line 618 of file std_code.h.

◆ to_code_assert() [2/2]

code_assertt& to_code_assert ( codet code)
inline

Definition at line 626 of file std_code.h.

◆ to_code_assign() [1/2]

const code_assignt& to_code_assign ( const codet code)
inline

Definition at line 381 of file std_code.h.

◆ to_code_assign() [2/2]

code_assignt& to_code_assign ( codet code)
inline

Definition at line 388 of file std_code.h.

◆ to_code_assume() [1/2]

const code_assumet& to_code_assume ( const codet code)
inline

Definition at line 566 of file std_code.h.

◆ to_code_assume() [2/2]

code_assumet& to_code_assume ( codet code)
inline

Definition at line 574 of file std_code.h.

◆ to_code_block() [1/2]

const code_blockt& to_code_block ( const codet code)
inline

Definition at line 254 of file std_code.h.

◆ to_code_block() [2/2]

code_blockt& to_code_block ( codet code)
inline

Definition at line 260 of file std_code.h.

◆ to_code_break() [1/2]

const code_breakt& to_code_break ( const codet code)
inline

Definition at line 1626 of file std_code.h.

◆ to_code_break() [2/2]

code_breakt& to_code_break ( codet code)
inline

Definition at line 1632 of file std_code.h.

◆ to_code_continue() [1/2]

const code_continuet& to_code_continue ( const codet code)
inline

Definition at line 1662 of file std_code.h.

◆ to_code_continue() [2/2]

code_continuet& to_code_continue ( codet code)
inline

Definition at line 1668 of file std_code.h.

◆ to_code_dead() [1/2]

const code_deadt& to_code_dead ( const codet code)
inline

Definition at line 517 of file std_code.h.

◆ to_code_dead() [2/2]

code_deadt& to_code_dead ( codet code)
inline

Definition at line 524 of file std_code.h.

◆ to_code_decl() [1/2]

const code_declt& to_code_decl ( const codet code)
inline

Definition at line 448 of file std_code.h.

◆ to_code_decl() [2/2]

code_declt& to_code_decl ( codet code)
inline

Definition at line 455 of file std_code.h.

◆ to_code_dowhile() [1/2]

const code_dowhilet& to_code_dowhile ( const codet code)
inline

Definition at line 1012 of file std_code.h.

◆ to_code_dowhile() [2/2]

code_dowhilet& to_code_dowhile ( codet code)
inline

Definition at line 1020 of file std_code.h.

◆ to_code_expression() [1/2]

code_expressiont& to_code_expression ( codet code)
inline

Definition at line 1851 of file std_code.h.

◆ to_code_expression() [2/2]

const code_expressiont& to_code_expression ( const codet code)
inline

Definition at line 1859 of file std_code.h.

◆ to_code_for() [1/2]

const code_fort& to_code_for ( const codet code)
inline

Definition at line 1109 of file std_code.h.

◆ to_code_for() [2/2]

code_fort& to_code_for ( codet code)
inline

Definition at line 1117 of file std_code.h.

◆ to_code_function_body() [1/2]

const code_function_bodyt& to_code_function_body ( const codet code)
inline

Definition at line 2510 of file std_code.h.

◆ to_code_function_body() [2/2]

code_function_bodyt& to_code_function_body ( codet code)
inline

Definition at line 2518 of file std_code.h.

◆ to_code_function_call() [1/2]

const code_function_callt& to_code_function_call ( const codet code)
inline

Definition at line 1294 of file std_code.h.

◆ to_code_function_call() [2/2]

code_function_callt& to_code_function_call ( codet code)
inline

Definition at line 1301 of file std_code.h.

◆ to_code_gcc_switch_case_range() [1/2]

const code_gcc_switch_case_ranget& to_code_gcc_switch_case_range ( const codet code)
inline

Definition at line 1584 of file std_code.h.

◆ to_code_gcc_switch_case_range() [2/2]

code_gcc_switch_case_ranget& to_code_gcc_switch_case_range ( codet code)
inline

Definition at line 1593 of file std_code.h.

◆ to_code_goto() [1/2]

const code_gotot& to_code_goto ( const codet code)
inline

Definition at line 1161 of file std_code.h.

◆ to_code_goto() [2/2]

code_gotot& to_code_goto ( codet code)
inline

Definition at line 1169 of file std_code.h.

◆ to_code_ifthenelse() [1/2]

const code_ifthenelset& to_code_ifthenelse ( const codet code)
inline

Definition at line 826 of file std_code.h.

◆ to_code_ifthenelse() [2/2]

code_ifthenelset& to_code_ifthenelse ( codet code)
inline

Definition at line 834 of file std_code.h.

◆ to_code_label() [1/2]

const code_labelt& to_code_label ( const codet code)
inline

Definition at line 1427 of file std_code.h.

◆ to_code_label() [2/2]

code_labelt& to_code_label ( codet code)
inline

Definition at line 1435 of file std_code.h.

◆ to_code_landingpad() [1/2]

static code_landingpadt& to_code_landingpad ( codet code)
inlinestatic

Definition at line 2376 of file std_code.h.

◆ to_code_landingpad() [2/2]

static const code_landingpadt& to_code_landingpad ( const codet code)
inlinestatic

Definition at line 2382 of file std_code.h.

◆ to_code_pop_catch() [1/2]

static code_pop_catcht& to_code_pop_catch ( codet code)
inlinestatic

Definition at line 2324 of file std_code.h.

◆ to_code_pop_catch() [2/2]

static const code_pop_catcht& to_code_pop_catch ( const codet code)
inlinestatic

Definition at line 2330 of file std_code.h.

◆ to_code_push_catch() [1/2]

static code_push_catcht& to_code_push_catch ( codet code)
inlinestatic

Definition at line 2287 of file std_code.h.

◆ to_code_push_catch() [2/2]

static const code_push_catcht& to_code_push_catch ( const codet code)
inlinestatic

Definition at line 2293 of file std_code.h.

◆ to_code_return() [1/2]

const code_returnt& to_code_return ( const codet code)
inline

Definition at line 1359 of file std_code.h.

◆ to_code_return() [2/2]

code_returnt& to_code_return ( codet code)
inline

Definition at line 1366 of file std_code.h.

◆ to_code_switch() [1/2]

const code_switcht& to_code_switch ( const codet code)
inline

Definition at line 888 of file std_code.h.

◆ to_code_switch() [2/2]

code_switcht& to_code_switch ( codet code)
inline

Definition at line 896 of file std_code.h.

◆ to_code_switch_case() [1/2]

const code_switch_caset& to_code_switch_case ( const codet code)
inline

Definition at line 1500 of file std_code.h.

◆ to_code_switch_case() [2/2]

code_switch_caset& to_code_switch_case ( codet code)
inline

Definition at line 1508 of file std_code.h.

◆ to_code_try_catch() [1/2]

const code_try_catcht& to_code_try_catch ( const codet code)
inline

Definition at line 2460 of file std_code.h.

◆ to_code_try_catch() [2/2]

code_try_catcht& to_code_try_catch ( codet code)
inline

Definition at line 2468 of file std_code.h.

◆ to_code_while() [1/2]

const code_whilet& to_code_while ( const codet code)
inline

Definition at line 950 of file std_code.h.

◆ to_code_while() [2/2]

code_whilet& to_code_while ( codet code)
inline

Definition at line 958 of file std_code.h.

◆ to_side_effect_expr() [1/2]

side_effect_exprt& to_side_effect_expr ( exprt expr)
inline

Definition at line 1938 of file std_code.h.

◆ to_side_effect_expr() [2/2]

const side_effect_exprt& to_side_effect_expr ( const exprt expr)
inline

Definition at line 1944 of file std_code.h.

◆ to_side_effect_expr_assign() [1/2]

side_effect_expr_assignt& to_side_effect_expr_assign ( exprt expr)
inline

Definition at line 2061 of file std_code.h.

◆ to_side_effect_expr_assign() [2/2]

const side_effect_expr_assignt& to_side_effect_expr_assign ( const exprt expr)
inline

Definition at line 2069 of file std_code.h.

◆ to_side_effect_expr_function_call() [1/2]

side_effect_expr_function_callt& to_side_effect_expr_function_call ( exprt expr)
inline

Definition at line 2143 of file std_code.h.

◆ to_side_effect_expr_function_call() [2/2]

const side_effect_expr_function_callt& to_side_effect_expr_function_call ( const exprt expr)
inline

Definition at line 2151 of file std_code.h.

◆ to_side_effect_expr_nondet() [1/2]

side_effect_expr_nondett& to_side_effect_expr_nondet ( exprt expr)
inline

Definition at line 1991 of file std_code.h.

◆ to_side_effect_expr_nondet() [2/2]

const side_effect_expr_nondett& to_side_effect_expr_nondet ( const exprt expr)
inline

Definition at line 1998 of file std_code.h.

◆ to_side_effect_expr_throw() [1/2]

side_effect_expr_throwt& to_side_effect_expr_throw ( exprt expr)
inline

Definition at line 2182 of file std_code.h.

◆ to_side_effect_expr_throw() [2/2]

const side_effect_expr_throwt& to_side_effect_expr_throw ( const exprt expr)
inline

Definition at line 2189 of file std_code.h.

◆ validate_expr() [1/21]

void validate_expr ( const code_assignt x)
inline

Definition at line 376 of file std_code.h.

◆ validate_expr() [2/21]

void validate_expr ( const code_declt x)
inline

Definition at line 443 of file std_code.h.

◆ validate_expr() [3/21]

void validate_expr ( const code_deadt x)
inline

Definition at line 512 of file std_code.h.

◆ validate_expr() [4/21]

void validate_expr ( const code_assumet x)
inline

Definition at line 561 of file std_code.h.

◆ validate_expr() [5/21]

void validate_expr ( const code_assertt x)
inline

Definition at line 613 of file std_code.h.

◆ validate_expr() [6/21]

void validate_expr ( const code_inputt input)
inline

Definition at line 676 of file std_code.h.

◆ validate_expr() [7/21]

void validate_expr ( const code_outputt output)
inline

Definition at line 722 of file std_code.h.

◆ validate_expr() [8/21]

void validate_expr ( const code_ifthenelset x)
inline

Definition at line 821 of file std_code.h.

◆ validate_expr() [9/21]

void validate_expr ( const code_switcht x)
inline

Definition at line 883 of file std_code.h.

◆ validate_expr() [10/21]

void validate_expr ( const code_whilet x)
inline

Definition at line 945 of file std_code.h.

◆ validate_expr() [11/21]

void validate_expr ( const code_dowhilet x)
inline

Definition at line 1007 of file std_code.h.

◆ validate_expr() [12/21]

void validate_expr ( const code_fort x)
inline

Definition at line 1104 of file std_code.h.

◆ validate_expr() [13/21]

void validate_expr ( const code_gotot x)
inline

Definition at line 1156 of file std_code.h.

◆ validate_expr() [14/21]

void validate_expr ( const code_function_callt x)
inline

Definition at line 1289 of file std_code.h.

◆ validate_expr() [15/21]

void validate_expr ( const code_returnt x)
inline

Definition at line 1354 of file std_code.h.

◆ validate_expr() [16/21]

void validate_expr ( const code_labelt x)
inline

Definition at line 1422 of file std_code.h.

◆ validate_expr() [17/21]

void validate_expr ( const code_switch_caset x)
inline

Definition at line 1495 of file std_code.h.

◆ validate_expr() [18/21]

void validate_expr ( const code_gcc_switch_case_ranget x)
inline

Definition at line 1578 of file std_code.h.

◆ validate_expr() [19/21]

void validate_expr ( const code_asm_gcct x)
inline

Definition at line 1791 of file std_code.h.

◆ validate_expr() [20/21]

void validate_expr ( const code_expressiont x)
inline

Definition at line 1846 of file std_code.h.

◆ validate_expr() [21/21]

void validate_expr ( const code_try_catcht x)
inline

Definition at line 2455 of file std_code.h.