std_code.h File Reference

#include <list>
#include "std_code_base.h"
#include "std_expr.h"

Include dependency graph for std_code.h:

Go to the source code of this file.

Classes
class	code_frontend_assignt
	A codet representing an assignment in the program. More...
class	code_blockt
	A codet representing sequential composition of program statements. 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_skipt
	A codet representing a skip statement. More...
class	code_frontend_declt
	A codet representing the declaration of a local variable. 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_frontend_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 ... When used in a GOTO program statement, the corresponding opcode must be CATCH, and the statement's targets must be in one-to-one correspondence with the exception tags. 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
namespace	detail

Functions
template<>
bool	can_cast_expr< code_frontend_assignt > (const exprt &base)
void	validate_expr (const code_frontend_assignt &x)
const code_frontend_assignt &	to_code_frontend_assign (const codet &code)
code_frontend_assignt &	to_code_frontend_assign (codet &code)
template<>
bool	can_cast_expr< code_blockt > (const exprt &base)
const code_blockt &	to_code_block (const codet &code)
code_blockt &	to_code_block (codet &code)
template<>
bool	can_cast_expr< code_assumet > (const exprt &base)
void	validate_expr (const code_assumet &x)
const code_assumet &	to_code_assume (const codet &code)
code_assumet &	to_code_assume (codet &code)
template<>
bool	can_cast_expr< code_assertt > (const exprt &base)
void	validate_expr (const code_assertt &x)
const code_assertt &	to_code_assert (const codet &code)
code_assertt &	to_code_assert (codet &code)
template<>
bool	can_cast_expr< code_skipt > (const exprt &base)
template<>
bool	can_cast_expr< code_frontend_declt > (const exprt &base)
void	validate_expr (const code_frontend_declt &x)
const code_frontend_declt &	to_code_frontend_decl (const codet &code)
code_frontend_declt &	to_code_frontend_decl (codet &code)
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.
template<>
bool	can_cast_expr< code_ifthenelset > (const exprt &base)
void	validate_expr (const code_ifthenelset &x)
const code_ifthenelset &	to_code_ifthenelse (const codet &code)
code_ifthenelset &	to_code_ifthenelse (codet &code)
template<>
bool	can_cast_expr< code_switcht > (const exprt &base)
void	validate_expr (const code_switcht &x)
const code_switcht &	to_code_switch (const codet &code)
code_switcht &	to_code_switch (codet &code)
template<>
bool	can_cast_expr< code_whilet > (const exprt &base)
void	validate_expr (const code_whilet &x)
const code_whilet &	to_code_while (const codet &code)
code_whilet &	to_code_while (codet &code)
template<>
bool	can_cast_expr< code_dowhilet > (const exprt &base)
void	validate_expr (const code_dowhilet &x)
const code_dowhilet &	to_code_dowhile (const codet &code)
code_dowhilet &	to_code_dowhile (codet &code)
template<>
bool	can_cast_expr< code_fort > (const exprt &base)
void	validate_expr (const code_fort &x)
const code_fort &	to_code_for (const codet &code)
code_fort &	to_code_for (codet &code)
template<>
bool	can_cast_expr< code_gotot > (const exprt &base)
void	validate_expr (const code_gotot &x)
const code_gotot &	to_code_goto (const codet &code)
code_gotot &	to_code_goto (codet &code)
template<>
bool	can_cast_expr< code_frontend_returnt > (const exprt &base)
void	validate_expr (const code_frontend_returnt &x)
const code_frontend_returnt &	to_code_frontend_return (const codet &code)
code_frontend_returnt &	to_code_frontend_return (codet &code)
template<>
bool	can_cast_expr< code_labelt > (const exprt &base)
void	validate_expr (const code_labelt &x)
const code_labelt &	to_code_label (const codet &code)
code_labelt &	to_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_caset &	to_code_switch_case (const codet &code)
code_switch_caset &	to_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_ranget &	to_code_gcc_switch_case_range (const codet &code)
code_gcc_switch_case_ranget &	to_code_gcc_switch_case_range (codet &code)
template<>
bool	can_cast_expr< code_breakt > (const exprt &base)
const code_breakt &	to_code_break (const codet &code)
code_breakt &	to_code_break (codet &code)
template<>
bool	can_cast_expr< code_continuet > (const exprt &base)
const code_continuet &	to_code_continue (const codet &code)
code_continuet &	to_code_continue (codet &code)
template<>
bool	can_cast_expr< code_asmt > (const exprt &base)
code_asmt &	to_code_asm (codet &code)
const code_asmt &	to_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_gcct &	to_code_asm_gcc (codet &code)
const code_asm_gcct &	to_code_asm_gcc (const codet &code)
template<>
bool	can_cast_expr< code_expressiont > (const exprt &base)
void	validate_expr (const code_expressiont &x)
code_expressiont &	to_code_expression (codet &code)
const code_expressiont &	to_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_exprt &	to_side_effect_expr (exprt &expr)
const side_effect_exprt &	to_side_effect_expr (const exprt &expr)
template<>
bool	can_cast_expr< side_effect_expr_nondett > (const exprt &base)
side_effect_expr_nondett &	to_side_effect_expr_nondet (exprt &expr)
const side_effect_expr_nondett &	to_side_effect_expr_nondet (const exprt &expr)
template<>
bool	can_cast_expr< side_effect_expr_assignt > (const exprt &base)
side_effect_expr_assignt &	to_side_effect_expr_assign (exprt &expr)
const side_effect_expr_assignt &	to_side_effect_expr_assign (const exprt &expr)
template<>
bool	can_cast_expr< side_effect_expr_statement_expressiont > (const exprt &base)
side_effect_expr_statement_expressiont &	to_side_effect_expr_statement_expression (exprt &expr)
const side_effect_expr_statement_expressiont &	to_side_effect_expr_statement_expression (const exprt &expr)
template<>
bool	can_cast_expr< side_effect_expr_function_callt > (const exprt &base)
side_effect_expr_function_callt &	to_side_effect_expr_function_call (exprt &expr)
const side_effect_expr_function_callt &	to_side_effect_expr_function_call (const exprt &expr)
template<>
bool	can_cast_expr< side_effect_expr_throwt > (const exprt &base)
side_effect_expr_throwt &	to_side_effect_expr_throw (exprt &expr)
const side_effect_expr_throwt &	to_side_effect_expr_throw (const exprt &expr)
template<>
bool	can_cast_expr< code_push_catcht > (const exprt &base)
static code_push_catcht &	to_code_push_catch (codet &code)
static const code_push_catcht &	to_code_push_catch (const codet &code)
template<>
bool	can_cast_expr< code_pop_catcht > (const exprt &base)
static code_pop_catcht &	to_code_pop_catch (codet &code)
static const code_pop_catcht &	to_code_pop_catch (const codet &code)
template<>
bool	can_cast_expr< code_landingpadt > (const exprt &base)
static code_landingpadt &	to_code_landingpad (codet &code)
static const code_landingpadt &	to_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_catcht &	to_code_try_catch (const codet &code)
code_try_catcht &	to_code_try_catch (codet &code)
const code_function_bodyt &	to_code_function_body (const codet &code)
code_function_bodyt &	to_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 1363 of file std_code.h.

can_cast_expr< code_asmt >()

template<>

bool can_cast_expr< code_asmt > ( const exprt &  base )

inline

Definition at line 1274 of file std_code.h.

can_cast_expr< code_assertt >()

template<>

bool can_cast_expr< code_assertt > ( const exprt &  base )

inline

Definition at line 294 of file std_code.h.

can_cast_expr< code_assumet >()

template<>

bool can_cast_expr< code_assumet > ( const exprt &  base )

inline

Definition at line 241 of file std_code.h.

can_cast_expr< code_blockt >()

template<>

bool can_cast_expr< code_blockt > ( const exprt &  base )

inline

Definition at line 195 of file std_code.h.

can_cast_expr< code_breakt >()

template<>

bool can_cast_expr< code_breakt > ( const exprt &  base )

inline

Definition at line 1195 of file std_code.h.

can_cast_expr< code_continuet >()

template<>

bool can_cast_expr< code_continuet > ( const exprt &  base )

inline

Definition at line 1231 of file std_code.h.

can_cast_expr< code_dowhilet >()

template<>

bool can_cast_expr< code_dowhilet > ( const exprt &  base )

inline

Definition at line 706 of file std_code.h.

can_cast_expr< code_expressiont >()

template<>

bool can_cast_expr< code_expressiont > ( const exprt &  base )

inline

Definition at line 1418 of file std_code.h.

can_cast_expr< code_fort >()

template<>

bool can_cast_expr< code_fort > ( const exprt &  base )

inline

Definition at line 813 of file std_code.h.

can_cast_expr< code_frontend_assignt >()

template<>

bool can_cast_expr< code_frontend_assignt > ( const exprt &  base )

inline

Definition at line 103 of file std_code.h.

can_cast_expr< code_frontend_declt >()

template<>

bool can_cast_expr< code_frontend_declt > ( const exprt &  base )

inline

Definition at line 419 of file std_code.h.

can_cast_expr< code_frontend_returnt >()

template<>

bool can_cast_expr< code_frontend_returnt > ( const exprt &  base )

inline

Definition at line 933 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 1150 of file std_code.h.

can_cast_expr< code_gotot >()

template<>

bool can_cast_expr< code_gotot > ( const exprt &  base )

inline

Definition at line 865 of file std_code.h.

can_cast_expr< code_ifthenelset >()

template<>

bool can_cast_expr< code_ifthenelset > ( const exprt &  base )

inline

Definition at line 520 of file std_code.h.

can_cast_expr< code_labelt >()

template<>

bool can_cast_expr< code_labelt > ( const exprt &  base )

inline

Definition at line 994 of file std_code.h.

can_cast_expr< code_landingpadt >()

template<>

bool can_cast_expr< code_landingpadt > ( const exprt &  base )

inline

Definition at line 1964 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 1912 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 1875 of file std_code.h.

can_cast_expr< code_skipt >()

template<>

bool can_cast_expr< code_skipt > ( const exprt &  base )

inline

Definition at line 335 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 1067 of file std_code.h.

can_cast_expr< code_switcht >()

template<>

bool can_cast_expr< code_switcht > ( const exprt &  base )

inline

Definition at line 582 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 2040 of file std_code.h.

can_cast_expr< code_whilet >()

template<>

bool can_cast_expr< code_whilet > ( const exprt &  base )

inline

Definition at line 644 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 1613 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 1730 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 1540 of file std_code.h.

can_cast_expr< side_effect_expr_statement_expressiont >()

template<>

bool can_cast_expr< side_effect_expr_statement_expressiont > ( const exprt &  base )

inline

Definition at line 1662 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 1770 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 1498 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

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.

Returns

A code block that asserts a condition then aborts if it does not hold.

Definition at line 120 of file std_code.cpp.

to_code_asm() [1/2]

code_asmt & to_code_asm ( codet &  code )

inline

Definition at line 1282 of file std_code.h.

to_code_asm() [2/2]

const code_asmt & to_code_asm ( const codet &  code )

inline

Definition at line 1288 of file std_code.h.

to_code_asm_gcc() [1/2]

code_asm_gcct & to_code_asm_gcc ( codet &  code )

inline

Definition at line 1373 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 1382 of file std_code.h.

to_code_assert() [1/2]

code_assertt & to_code_assert ( codet &  code )

inline

Definition at line 312 of file std_code.h.

to_code_assert() [2/2]

const code_assertt & to_code_assert ( const codet &  code )

inline

Definition at line 304 of file std_code.h.

to_code_assume() [1/2]

code_assumet & to_code_assume ( codet &  code )

inline

Definition at line 259 of file std_code.h.

to_code_assume() [2/2]

const code_assumet & to_code_assume ( const codet &  code )

inline

Definition at line 251 of file std_code.h.

to_code_block() [1/2]

code_blockt & to_code_block ( codet &  code )

inline

Definition at line 209 of file std_code.h.

to_code_block() [2/2]

const code_blockt & to_code_block ( const codet &  code )

inline

Definition at line 203 of file std_code.h.

to_code_break() [1/2]

code_breakt & to_code_break ( codet &  code )

inline

Definition at line 1209 of file std_code.h.

to_code_break() [2/2]

const code_breakt & to_code_break ( const codet &  code )

inline

Definition at line 1203 of file std_code.h.

to_code_continue() [1/2]

code_continuet & to_code_continue ( codet &  code )

inline

Definition at line 1245 of file std_code.h.

to_code_continue() [2/2]

const code_continuet & to_code_continue ( const codet &  code )

inline

Definition at line 1239 of file std_code.h.

to_code_dowhile() [1/2]

code_dowhilet & to_code_dowhile ( codet &  code )

inline

Definition at line 724 of file std_code.h.

to_code_dowhile() [2/2]

const code_dowhilet & to_code_dowhile ( const codet &  code )

inline

Definition at line 716 of file std_code.h.

to_code_expression() [1/2]

code_expressiont & to_code_expression ( codet &  code )

inline

Definition at line 1428 of file std_code.h.

to_code_expression() [2/2]

const code_expressiont & to_code_expression ( const codet &  code )

inline

Definition at line 1436 of file std_code.h.

to_code_for() [1/2]

code_fort & to_code_for ( codet &  code )

inline

Definition at line 831 of file std_code.h.

to_code_for() [2/2]

const code_fort & to_code_for ( const codet &  code )

inline

Definition at line 823 of file std_code.h.

to_code_frontend_assign() [1/2]

code_frontend_assignt & to_code_frontend_assign ( codet &  code )

inline

Definition at line 120 of file std_code.h.

to_code_frontend_assign() [2/2]

const code_frontend_assignt & to_code_frontend_assign ( const codet &  code )

inline

Definition at line 113 of file std_code.h.

to_code_frontend_decl() [1/2]

code_frontend_declt & to_code_frontend_decl ( codet &  code )

inline

Definition at line 436 of file std_code.h.

to_code_frontend_decl() [2/2]

const code_frontend_declt & to_code_frontend_decl ( const codet &  code )

inline

Definition at line 429 of file std_code.h.

to_code_frontend_return() [1/2]

code_frontend_returnt & to_code_frontend_return ( codet &  code )

inline

Definition at line 950 of file std_code.h.

to_code_frontend_return() [2/2]

const code_frontend_returnt & to_code_frontend_return ( const codet &  code )

inline

Definition at line 943 of file std_code.h.

to_code_function_body() [1/2]

code_function_bodyt & to_code_function_body ( codet &  code )

inline

Definition at line 2108 of file std_code.h.

to_code_function_body() [2/2]

const code_function_bodyt & to_code_function_body ( const codet &  code )

inline

Definition at line 2100 of file std_code.h.

to_code_gcc_switch_case_range() [1/2]

code_gcc_switch_case_ranget & to_code_gcc_switch_case_range ( codet &  code )

inline

Definition at line 1170 of file std_code.h.

to_code_gcc_switch_case_range() [2/2]

const code_gcc_switch_case_ranget & to_code_gcc_switch_case_range ( const codet &  code )

inline

Definition at line 1161 of file std_code.h.

to_code_goto() [1/2]

code_gotot & to_code_goto ( codet &  code )

inline

Definition at line 883 of file std_code.h.

to_code_goto() [2/2]

const code_gotot & to_code_goto ( const codet &  code )

inline

Definition at line 875 of file std_code.h.

to_code_ifthenelse() [1/2]

code_ifthenelset & to_code_ifthenelse ( codet &  code )

inline

Definition at line 538 of file std_code.h.

to_code_ifthenelse() [2/2]

const code_ifthenelset & to_code_ifthenelse ( const codet &  code )

inline

Definition at line 530 of file std_code.h.

to_code_label() [1/2]

code_labelt & to_code_label ( codet &  code )

inline

Definition at line 1012 of file std_code.h.

to_code_label() [2/2]

const code_labelt & to_code_label ( const codet &  code )

inline

Definition at line 1004 of file std_code.h.

to_code_landingpad() [1/2]

static code_landingpadt & to_code_landingpad ( codet &  code )

inlinestatic

Definition at line 1972 of file std_code.h.

to_code_landingpad() [2/2]

static const code_landingpadt & to_code_landingpad ( const codet &  code )

inlinestatic

Definition at line 1978 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 1920 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 1926 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 1883 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 1889 of file std_code.h.

to_code_switch() [1/2]

code_switcht & to_code_switch ( codet &  code )

inline

Definition at line 600 of file std_code.h.

to_code_switch() [2/2]

const code_switcht & to_code_switch ( const codet &  code )

inline

Definition at line 592 of file std_code.h.

to_code_switch_case() [1/2]

code_switch_caset & to_code_switch_case ( codet &  code )

inline

Definition at line 1085 of file std_code.h.

to_code_switch_case() [2/2]

const code_switch_caset & to_code_switch_case ( const codet &  code )

inline

Definition at line 1077 of file std_code.h.

to_code_try_catch() [1/2]

code_try_catcht & to_code_try_catch ( codet &  code )

inline

Definition at line 2058 of file std_code.h.

to_code_try_catch() [2/2]

const code_try_catcht & to_code_try_catch ( const codet &  code )

inline

Definition at line 2050 of file std_code.h.

to_code_while() [1/2]

code_whilet & to_code_while ( codet &  code )

inline

Definition at line 662 of file std_code.h.

to_code_while() [2/2]

const code_whilet & to_code_while ( const codet &  code )

inline

Definition at line 654 of file std_code.h.

to_side_effect_expr() [1/2]

const side_effect_exprt & to_side_effect_expr ( const exprt &  expr )

inline

Definition at line 1512 of file std_code.h.

to_side_effect_expr() [2/2]

side_effect_exprt & to_side_effect_expr ( exprt &  expr )

inline

Definition at line 1506 of file std_code.h.

to_side_effect_expr_assign() [1/2]

const side_effect_expr_assignt & to_side_effect_expr_assign ( const exprt &  expr )

inline

Definition at line 1626 of file std_code.h.

to_side_effect_expr_assign() [2/2]

side_effect_expr_assignt & to_side_effect_expr_assign ( exprt &  expr )

inline

Definition at line 1618 of file std_code.h.

to_side_effect_expr_function_call() [1/2]

const side_effect_expr_function_callt & to_side_effect_expr_function_call ( const exprt &  expr )

inline

Definition at line 1747 of file std_code.h.

to_side_effect_expr_function_call() [2/2]

side_effect_expr_function_callt & to_side_effect_expr_function_call ( exprt &  expr )

inline

Definition at line 1739 of file std_code.h.

to_side_effect_expr_nondet() [1/2]

const side_effect_expr_nondett & to_side_effect_expr_nondet ( const exprt &  expr )

inline

Definition at line 1555 of file std_code.h.

to_side_effect_expr_nondet() [2/2]

side_effect_expr_nondett & to_side_effect_expr_nondet ( exprt &  expr )

inline

Definition at line 1548 of file std_code.h.

to_side_effect_expr_statement_expression() [1/2]

const side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression ( const exprt &  expr )

inline

Definition at line 1680 of file std_code.h.

to_side_effect_expr_statement_expression() [2/2]

side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression ( exprt &  expr )

inline

Definition at line 1669 of file std_code.h.

to_side_effect_expr_throw() [1/2]

const side_effect_expr_throwt & to_side_effect_expr_throw ( const exprt &  expr )

inline

Definition at line 1785 of file std_code.h.

to_side_effect_expr_throw() [2/2]

side_effect_expr_throwt & to_side_effect_expr_throw ( exprt &  expr )

inline

Definition at line 1778 of file std_code.h.

validate_expr() [1/17]

void validate_expr ( const code_asm_gcct &  x )

inline

Definition at line 1368 of file std_code.h.

validate_expr() [2/17]

void validate_expr ( const code_assertt &  x )

inline

Definition at line 299 of file std_code.h.

validate_expr() [3/17]

void validate_expr ( const code_assumet &  x )

inline

Definition at line 246 of file std_code.h.

validate_expr() [4/17]

void validate_expr ( const code_dowhilet &  x )

inline

Definition at line 711 of file std_code.h.

validate_expr() [5/17]

void validate_expr ( const code_expressiont &  x )

inline

Definition at line 1423 of file std_code.h.

validate_expr() [6/17]

void validate_expr ( const code_fort &  x )

inline

Definition at line 818 of file std_code.h.

validate_expr() [7/17]

void validate_expr ( const code_frontend_assignt &  x )

inline

Definition at line 108 of file std_code.h.

validate_expr() [8/17]

void validate_expr ( const code_frontend_declt &  x )

inline

Definition at line 424 of file std_code.h.

validate_expr() [9/17]

void validate_expr ( const code_frontend_returnt &  x )

inline

Definition at line 938 of file std_code.h.

validate_expr() [10/17]

void validate_expr ( const code_gcc_switch_case_ranget &  x )

inline

Definition at line 1155 of file std_code.h.

validate_expr() [11/17]

void validate_expr ( const code_gotot &  x )

inline

Definition at line 870 of file std_code.h.

validate_expr() [12/17]

void validate_expr ( const code_ifthenelset &  x )

inline

Definition at line 525 of file std_code.h.

validate_expr() [13/17]

void validate_expr ( const code_labelt &  x )

inline

Definition at line 999 of file std_code.h.

validate_expr() [14/17]

void validate_expr ( const code_switch_caset &  x )

inline

Definition at line 1072 of file std_code.h.

validate_expr() [15/17]

void validate_expr ( const code_switcht &  x )

inline

Definition at line 587 of file std_code.h.

validate_expr() [16/17]

void validate_expr ( const code_try_catcht &  x )

inline

Definition at line 2045 of file std_code.h.

validate_expr() [17/17]

void validate_expr ( const code_whilet &  x )

inline

Definition at line 649 of file std_code.h.