cprover
std_code.h File Reference
#include <cassert>
#include <list>
#include "expr.h"
#include "expr_cast.h"
Include dependency graph for std_code.h:

Go to the source code of this file.

Classes

class  codet
 A statement in a programming language. More...
 
class  code_blockt
 Sequential composition. More...
 
class  code_skipt
 Skip. More...
 
class  code_assignt
 Assignment. More...
 
class  code_declt
 A declaration of a local variable. More...
 
class  code_deadt
 A removal of a local variable. 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
 An if-then-else. More...
 
class  code_switcht
 A ‘switch’ instruction. More...
 
class  code_whilet
 A ‘while’ instruction. More...
 
class  code_dowhilet
 A ‘do while’ instruction. More...
 
class  code_fort
 A ‘for’ instruction. More...
 
class  code_gotot
 A ‘goto’ instruction. More...
 
class  code_function_callt
 A function call. More...
 
class  code_returnt
 Return from a function. More...
 
class  code_labelt
 A label for branch targets. More...
 
class  code_switch_caset
 A switch-case. More...
 
class  code_breakt
 A break for ‘for’ and ‘while’ loops. More...
 
class  code_continuet
 A continue for ‘for’ and ‘while’ loops. More...
 
class  code_asmt
 An inline assembler statement. More...
 
class  code_expressiont
 An expression statement. More...
 
class  side_effect_exprt
 An expression containing a side effect. More...
 
class  side_effect_expr_nondett
 A side effect that returns a non-deterministically chosen value. More...
 
class  side_effect_expr_function_callt
 A function call side effect. More...
 
class  side_effect_expr_throwt
 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
 A try/catch block. 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)
 
const code_assumetto_code_assume (const codet &code)
 
code_assumetto_code_assume (codet &code)
 
template<>
bool can_cast_expr< code_assertt > (const exprt &base)
 
const code_asserttto_code_assert (const codet &code)
 
code_asserttto_code_assert (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. 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)
 
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)
 
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_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_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_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)
 

Function Documentation

◆ can_cast_expr< code_asmt >()

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

Definition at line 1198 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_assertt >()

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

Definition at line 429 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_assignt >()

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

Definition at line 230 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_assumet >()

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

Definition at line 382 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_blockt >()

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

Definition at line 157 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_breakt >()

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

Definition at line 1123 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_continuet >()

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

Definition at line 1153 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_deadt >()

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

Definition at line 334 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_declt >()

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

Definition at line 281 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_dowhilet >()

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

Definition at line 701 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_expressiont >()

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

Definition at line 1245 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_fort >()

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

Definition at line 777 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_function_callt >()

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

Definition at line 901 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_gotot >()

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

Definition at line 827 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_ifthenelset >()

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

Definition at line 512 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_labelt >()

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

Definition at line 1021 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_landingpadt >()

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

Definition at line 1685 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_pop_catcht >()

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

Definition at line 1640 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_push_catcht >()

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

Definition at line 1609 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_returnt >()

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

Definition at line 955 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_skipt >()

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

Definition at line 187 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_switch_caset >()

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

Definition at line 1091 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_switcht >()

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

Definition at line 575 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_try_catcht >()

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

Definition at line 1757 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< code_whilet >()

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

Definition at line 638 of file std_code.h.

References detail::can_cast_code_impl().

◆ can_cast_expr< codet >()

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

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

References detail::can_cast_side_effect_expr_impl().

◆ can_cast_expr< side_effect_expr_nondett >()

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

Definition at line 1370 of file std_code.h.

References detail::can_cast_side_effect_expr_impl().

Referenced by is_nondet_pointer().

◆ can_cast_expr< side_effect_expr_throwt >()

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

Definition at line 1510 of file std_code.h.

References detail::can_cast_side_effect_expr_impl().

◆ can_cast_expr< side_effect_exprt >()

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

Definition at line 1318 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 110 of file std_code.cpp.

References exprt::add_source_location(), exprt::copy_to_operands(), loc, and exprt::operands().

Referenced by java_bytecode_instrumentt::check_arithmetic_exception(), java_bytecode_instrumentt::check_array_access(), java_bytecode_instrumentt::check_array_length(), java_bytecode_instrumentt::check_class_cast(), and java_bytecode_instrumentt::check_null_dereference().

◆ to_code() [1/2]

const codet& to_code ( const exprt expr)
inline

Definition at line 75 of file std_code.h.

References irept::id().

Referenced by allocate_dynamic_object_with_decl(), code_blockt::append(), invariant_sett::apply_code(), value_sett::apply_code_rec(), code_switcht::body(), code_whilet::body(), code_dowhilet::body(), code_fort::body(), goto_program2codet::cleanup_code(), goto_program2codet::cleanup_code_block(), dump_ct::cleanup_expr(), dump_ct::cleanup_harness(), goto_convertt::convert(), goto_convertt::convert_block(), jsil_convertt::convert_code(), expr2ct::convert_code_block(), expr2ct::convert_code_decl_block(), expr2ct::convert_code_switch(), goto_convertt::convert_cpp_delete(), goto_convertt::convert_CPROVER_try_catch(), goto_convertt::convert_CPROVER_try_finally(), goto_convertt::convert_dowhile(), goto_convertt::convert_for(), goto_convert_functionst::convert_function(), cpp_typecheckt::convert_function(), goto_convertt::convert_gcc_switch_case_range(), goto_program2codet::convert_goto_switch(), goto_program2codet::convert_goto_while(), java_bytecode_convert_methodt::convert_instructions(), goto_convertt::convert_label(), goto_program2codet::convert_labels(), goto_convertt::convert_msc_try_except(), goto_convertt::convert_msc_try_finally(), expr2ct::convert_statement_expression(), convert_threadblock(), goto_convertt::convert_try_catch(), expr2javat::convert_with_precedence(), expr2ct::convert_with_precedence(), copy_parent(), cpp_typecheckt::cpp_constructor(), goto_convertt::cpp_new_initializer(), goto_convertt::do_printf(), find_block_position_rec(), code_blockt::find_last_statement(), codet::first_statement(), format_rec(), ci_lazy_methodst::gather_virtual_callsites(), require_goto_statements::get_all_statements(), code_try_catcht::get_catch_code(), code_try_catcht::get_catch_decl(), java_bytecode_convert_methodt::get_or_create_block_for_pcrange(), goto_convert(), has_labels(), insert_at_label(), mm2cppt::instruction2cpp(), java_bytecode_instrumentt::instrument_code(), instrument_synchronized_code(), java_bytecode_instrument(), java_bytecode_instrument_symbol(), java_static_lifetime_init(), codet::last_statement(), model_argc_argv(), monitor_exits(), move_label_ifthenelse(), cpp_typecheckt::move_member_initializers(), mm2cppt::operator()(), jsil_convertt::operator()(), goto_convertt::remove_assignment(), goto_convertt::remove_statement_expression(), goto_convertt::remove_temporary_object(), java_bytecode_convert_methodt::replace_goto_target(), static_lifetime_init(), jsil_typecheckt::typecheck_block(), c_typecheck_baset::typecheck_block(), java_bytecode_typecheckt::typecheck_code(), c_typecheck_baset::typecheck_code(), cpp_typecheckt::typecheck_compound_declarator(), java_bytecode_typecheckt::typecheck_expr(), c_typecheck_baset::typecheck_expr_operands(), c_typecheck_baset::typecheck_for(), c_typecheck_baset::typecheck_function_body(), c_typecheck_baset::typecheck_gcc_switch_case_range(), cpp_typecheckt::typecheck_ifthenelse(), jsil_typecheckt::typecheck_non_type_symbol(), c_typecheck_baset::typecheck_side_effect_statement_expression(), c_typecheck_baset::typecheck_start_thread(), cpp_typecheckt::typecheck_switch(), cpp_typecheckt::typecheck_try_catch(), cpp_typecheckt::typecheck_while(), and yyjsilparse().

◆ to_code() [2/2]

codet& to_code ( exprt expr)
inline

Definition at line 81 of file std_code.h.

References irept::id().

◆ to_code_asm() [1/2]

◆ to_code_asm() [2/2]

const code_asmt& to_code_asm ( const codet code)
inline

Definition at line 1212 of file std_code.h.

References codet::get_statement().

◆ to_code_assert() [1/2]

const code_assertt& to_code_assert ( const codet code)
inline

◆ to_code_assert() [2/2]

code_assertt& to_code_assert ( codet code)
inline

Definition at line 443 of file std_code.h.

References codet::get_statement().

◆ to_code_assign() [1/2]

const code_assignt& to_code_assign ( const codet code)
inline

Definition at line 240 of file std_code.h.

References codet::get_statement(), and exprt::operands().

Referenced by string_abstractiont::abstract_assign(), string_abstractiont::abstract_char_assign(), string_abstractiont::abstract_pointer_assign(), overflow_instrumentert::add_overflow_checks(), local_may_aliast::build(), local_bitvector_analysist::build(), check_and_replace_target(), cone_of_influencet::cone_of_influence(), polynomial_acceleratort::cone_of_influence(), goto_convertt::convert(), goto_program2codet::convert_assign(), goto_program2codet::convert_assign_varargs(), jsil_convertt::convert_code(), expr2ct::convert_code(), goto_program2codet::convert_decl(), goto_convertt::convert_init(), interpretert::execute_assign(), expressions_read(), expressions_written(), filter_out(), acceleration_utilst::find_modified(), require_goto_statements::find_pointer_assignments(), require_goto_statements::find_struct_component_assignments(), require_goto_statements::find_this_component_assignment(), scratch_programt::fix_types(), format_rec(), acceleration_utilst::gather_array_assignments(), get_modifies(), function_modifiest::get_modifies(), havoc_loopst::get_modifies(), goto_checkt::goto_check(), goto_rw(), implicit(), goto_inlinet::insert_function_body(), concurrency_instrumentationt::instrument(), escape_analysist::instrument(), java_bytecode_instrumentt::instrument_code(), is_assignment_from(), mm_io(), mutex_init_instrumentation(), nondet_static(), nondet_volatile(), does_remove_constt::operator()(), replace_callst::operator()(), acceleration_utilst::precondition(), polynomial_acceleratort::precondition(), print_global_state_size(), goto_convertt::remove_assignment(), goto_convertt::remove_statement_expression(), constant_propagator_ait::replace(), remove_returnst::restore_returns(), goto_program2codet::scan_for_varargs(), slice_global_inits(), static_simplifier(), goto_symext::symex_step(), constant_propagator_domaint::transform(), custom_bitvector_domaint::transform(), escape_domaint::transform(), global_may_alias_domaint::transform(), interval_domaint::transform(), invariant_set_domaint::transform(), java_bytecode_typecheckt::typecheck_code(), jsil_typecheckt::typecheck_code(), remove_returnst::undo_function_calls(), and wp().

◆ to_code_assign() [2/2]

code_assignt& to_code_assign ( codet code)
inline

Definition at line 246 of file std_code.h.

References codet::get_statement(), and exprt::operands().

◆ to_code_assume() [1/2]

const code_assumet& to_code_assume ( const codet code)
inline

Definition at line 390 of file std_code.h.

References codet::get_statement().

Referenced by value_sett::apply_code_rec(), goto_convertt::convert(), and wp().

◆ to_code_assume() [2/2]

code_assumet& to_code_assume ( codet code)
inline

Definition at line 396 of file std_code.h.

References codet::get_statement().

◆ to_code_block() [1/2]

◆ to_code_block() [2/2]

code_blockt& to_code_block ( codet code)
inline

Definition at line 171 of file std_code.h.

References codet::get_statement().

◆ to_code_break() [1/2]

const code_breakt& to_code_break ( const codet code)
inline

Definition at line 1131 of file std_code.h.

References codet::get_statement().

Referenced by goto_convertt::convert().

◆ to_code_break() [2/2]

code_breakt& to_code_break ( codet code)
inline

Definition at line 1137 of file std_code.h.

References codet::get_statement().

◆ to_code_continue() [1/2]

const code_continuet& to_code_continue ( const codet code)
inline

Definition at line 1161 of file std_code.h.

References codet::get_statement().

Referenced by goto_convertt::convert().

◆ to_code_continue() [2/2]

code_continuet& to_code_continue ( codet code)
inline

Definition at line 1167 of file std_code.h.

References codet::get_statement().

◆ to_code_dead() [1/2]

◆ to_code_dead() [2/2]

code_deadt& to_code_dead ( codet code)
inline

Definition at line 350 of file std_code.h.

References codet::get_statement(), and exprt::operands().

◆ to_code_decl() [1/2]

◆ to_code_decl() [2/2]

code_declt& to_code_decl ( codet code)
inline

Definition at line 298 of file std_code.h.

References codet::get_statement(), and exprt::operands().

◆ to_code_dowhile() [1/2]

const code_dowhilet& to_code_dowhile ( const codet code)
inline

◆ to_code_dowhile() [2/2]

code_dowhilet& to_code_dowhile ( codet code)
inline

Definition at line 718 of file std_code.h.

References codet::get_statement(), and exprt::operands().

◆ to_code_expression() [1/2]

◆ to_code_expression() [2/2]

const code_expressiont& to_code_expression ( const codet code)
inline

Definition at line 1262 of file std_code.h.

References codet::get_statement(), and exprt::operands().

◆ to_code_for() [1/2]

const code_fort& to_code_for ( const codet code)
inline

Definition at line 787 of file std_code.h.

References codet::get_statement(), and exprt::operands().

Referenced by goto_convertt::convert(), and expr2ct::convert_code().

◆ to_code_for() [2/2]

code_fort& to_code_for ( codet code)
inline

Definition at line 794 of file std_code.h.

References codet::get_statement(), and exprt::operands().

◆ to_code_function_call() [1/2]

const code_function_callt& to_code_function_call ( const codet code)
inline

Definition at line 909 of file std_code.h.

References codet::get_statement().

Referenced by string_abstractiont::abstract_function_call(), code_contractst::apply_contract(), local_may_aliast::build(), local_bitvector_analysist::build(), check_and_replace_target(), goto_program2codet::cleanup_code(), dump_ct::cleanup_expr(), dump_ct::cleanup_harness(), goto_checkt::collect_allocations(), _rw_set_loct::compute(), compute_called_functions(), cfg_baset< cfg_nodet >::compute_edges_function_call(), procedure_local_cfg_baset< nodet, goto_programt, goto_programt::targett >::compute_edges_function_call(), goto_convertt::convert(), expr2javat::convert_code(), expr2ct::convert_code(), goto_program2codet::convert_decl(), goto_program2codet::convert_start_thread(), convert_threadblock(), goto_program_dereferencet::dereference_instruction(), string_instrumentationt::do_function_call(), flow_insensitive_analysis_baset::do_function_call(), parameter_assignmentst::do_function_calls(), remove_returnst::do_function_calls(), interpretert::execute_function_call(), expressions_read(), expressions_written(), require_goto_statements::find_function_calls(), find_used_functions(), forall_callsites(), remove_exceptionst::function_or_callees_may_throw(), ci_lazy_methodst::gather_virtual_callsites(), goto_inlinet::get_call(), get_modifies(), function_modifiest::get_modifies(), havoc_loopst::get_modifies(), get_nondet_instruction_info(), flow_insensitive_abstract_domain_baset::get_return_lhs(), static_analysis_baset::get_return_lhs(), goto_checkt::goto_check(), goto_rw(), concurrency_instrumentationt::instrument(), taint_analysist::instrument(), cover_cover_instrumentert::instrument(), java_bytecode_instrumentt::instrument_code(), remove_exceptionst::instrument_function_call(), instrument_preconditions(), is_fence(), is_lwfence(), remove_calls_no_bodyt::is_opaque_function_call(), list_calls_and_arguments(), model_argc_argv(), nondet_static(), nondet_volatile(), remove_calls_no_bodyt::operator()(), replace_callst::operator()(), check_call_sequencet::operator()(), remove_function_pointerst::remove_function_pointer(), remove_function_pointerst::remove_function_pointers(), remove_virtual_functionst::remove_virtual_function(), remove_virtual_functionst::remove_virtual_functions(), constant_propagator_ait::replace(), show_call_sequences(), splice_call(), static_simplifier(), goto_symext::symex_step(), thread_exit_instrumentation(), constant_propagator_domaint::transform(), uncaught_exceptions_domaint::transform(), custom_bitvector_domaint::transform(), escape_domaint::transform(), interval_domaint::transform(), value_set_domain_fivrt::transform(), value_set_domain_fivrnst::transform(), value_set_domain_fit::transform(), rd_range_domaint::transform(), rd_range_domaint::transform_end_function(), rd_range_domaint::transform_function_call(), java_bytecode_typecheckt::typecheck_code(), jsil_typecheckt::typecheck_code(), c_typecheck_baset::typecheck_side_effect_statement_expression(), jsil_typecheckt::typecheck_try_catch(), undefined_function_abort_path(), remove_returnst::undo_function_calls(), flow_insensitive_analysis_baset::visit(), static_analysis_baset::visit(), ai_baset::visit(), instrumentert::cfg_visitort::visit_cfg_function_call(), and shared_bufferst::cfg_visitort::weak_memory().

◆ to_code_function_call() [2/2]

code_function_callt& to_code_function_call ( codet code)
inline

Definition at line 915 of file std_code.h.

References codet::get_statement().

◆ to_code_goto() [1/2]

const code_gotot& to_code_goto ( const codet code)
inline

◆ to_code_goto() [2/2]

code_gotot& to_code_goto ( codet code)
inline

Definition at line 844 of file std_code.h.

References codet::get_statement(), and exprt::operands().

◆ to_code_ifthenelse() [1/2]

◆ to_code_ifthenelse() [2/2]

code_ifthenelset& to_code_ifthenelse ( codet code)
inline

Definition at line 529 of file std_code.h.

References codet::get_statement(), and exprt::operands().

◆ to_code_label() [1/2]

◆ to_code_label() [2/2]

code_labelt& to_code_label ( codet code)
inline

Definition at line 1037 of file std_code.h.

References codet::get_statement(), and exprt::operands().

◆ to_code_landingpad() [1/2]

static code_landingpadt& to_code_landingpad ( codet code)
inlinestatic

◆ to_code_landingpad() [2/2]

static const code_landingpadt& to_code_landingpad ( const codet code)
inlinestatic

Definition at line 1699 of file std_code.h.

References codet::get_statement().

◆ to_code_pop_catch() [1/2]

static code_pop_catcht& to_code_pop_catch ( codet code)
inlinestatic

Definition at line 1648 of file std_code.h.

References codet::get_statement().

◆ to_code_pop_catch() [2/2]

static const code_pop_catcht& to_code_pop_catch ( const codet code)
inlinestatic

Definition at line 1654 of file std_code.h.

References codet::get_statement().

◆ to_code_push_catch() [1/2]

static code_push_catcht& to_code_push_catch ( codet code)
inlinestatic

◆ to_code_push_catch() [2/2]

static const code_push_catcht& to_code_push_catch ( const codet code)
inlinestatic

Definition at line 1623 of file std_code.h.

References codet::get_statement().

◆ to_code_return() [1/2]

◆ to_code_return() [2/2]

code_returnt& to_code_return ( codet code)
inline

Definition at line 969 of file std_code.h.

References codet::get_statement().

◆ to_code_switch() [1/2]

◆ to_code_switch() [2/2]

code_switcht& to_code_switch ( codet code)
inline

Definition at line 592 of file std_code.h.

References codet::get_statement(), and exprt::operands().

◆ to_code_switch_case() [1/2]

◆ to_code_switch_case() [2/2]

code_switch_caset& to_code_switch_case ( codet code)
inline

Definition at line 1107 of file std_code.h.

References codet::get_statement(), and exprt::operands().

◆ to_code_try_catch() [1/2]

const code_try_catcht& to_code_try_catch ( const codet code)
inline

Definition at line 1767 of file std_code.h.

References codet::get_statement(), and exprt::operands().

Referenced by jsil_typecheckt::typecheck_code().

◆ to_code_try_catch() [2/2]

code_try_catcht& to_code_try_catch ( codet code)
inline

Definition at line 1773 of file std_code.h.

References codet::get_statement(), and exprt::operands().

◆ to_code_while() [1/2]

const code_whilet& to_code_while ( const codet code)
inline

◆ to_code_while() [2/2]

code_whilet& to_code_while ( codet code)
inline

Definition at line 655 of file std_code.h.

References codet::get_statement(), and exprt::operands().

◆ to_side_effect_expr() [1/2]

◆ to_side_effect_expr() [2/2]

const side_effect_exprt& to_side_effect_expr ( const exprt expr)
inline

Definition at line 1332 of file std_code.h.

References irept::id().

◆ to_side_effect_expr_function_call() [1/2]

◆ 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 1482 of file std_code.h.

References irept::get(), and irept::id().

◆ to_side_effect_expr_nondet() [1/2]

side_effect_expr_nondett& to_side_effect_expr_nondet ( exprt expr)
inline

Definition at line 1378 of file std_code.h.

References to_side_effect_expr().

Referenced by insert_nondet_init_code().

◆ to_side_effect_expr_nondet() [2/2]

const side_effect_expr_nondett& to_side_effect_expr_nondet ( const exprt expr)
inline

Definition at line 1385 of file std_code.h.

References to_side_effect_expr().

◆ to_side_effect_expr_throw() [1/2]

side_effect_expr_throwt& to_side_effect_expr_throw ( exprt expr)
inline

Definition at line 1518 of file std_code.h.

References irept::get(), and irept::id().

Referenced by jsil_typecheckt::typecheck_expr_main().

◆ to_side_effect_expr_throw() [2/2]

const side_effect_expr_throwt& to_side_effect_expr_throw ( const exprt expr)
inline

Definition at line 1525 of file std_code.h.

References irept::get(), and irept::id().

◆ validate_expr() [1/13]

void validate_expr ( const code_assignt x)
inline

Definition at line 235 of file std_code.h.

References validate_operands().

◆ validate_expr() [2/13]

void validate_expr ( const code_declt x)
inline

Definition at line 286 of file std_code.h.

References validate_operands().

◆ validate_expr() [3/13]

void validate_expr ( const code_deadt x)
inline

Definition at line 339 of file std_code.h.

References validate_operands().

◆ validate_expr() [4/13]

void validate_expr ( const code_ifthenelset x)
inline

Definition at line 517 of file std_code.h.

References validate_operands().

◆ validate_expr() [5/13]

void validate_expr ( const code_switcht x)
inline

Definition at line 580 of file std_code.h.

References validate_operands().

◆ validate_expr() [6/13]

void validate_expr ( const code_whilet x)
inline

Definition at line 643 of file std_code.h.

References validate_operands().

◆ validate_expr() [7/13]

void validate_expr ( const code_dowhilet x)
inline

Definition at line 706 of file std_code.h.

References validate_operands().

◆ validate_expr() [8/13]

void validate_expr ( const code_fort x)
inline

Definition at line 782 of file std_code.h.

References validate_operands().

◆ validate_expr() [9/13]

void validate_expr ( const code_gotot x)
inline

Definition at line 832 of file std_code.h.

References validate_operands().

◆ validate_expr() [10/13]

void validate_expr ( const code_labelt x)
inline

Definition at line 1026 of file std_code.h.

References validate_operands().

◆ validate_expr() [11/13]

void validate_expr ( const code_switch_caset x)
inline

Definition at line 1096 of file std_code.h.

References validate_operands().

◆ validate_expr() [12/13]

void validate_expr ( const code_expressiont x)
inline

Definition at line 1250 of file std_code.h.

References validate_operands().

◆ validate_expr() [13/13]

void validate_expr ( const code_try_catcht x)
inline

Definition at line 1762 of file std_code.h.

References validate_operands().