goto_convert.cpp File Reference

#include <algorithm>
#include <cassert>
#include <map>
#include <goto-programs/destructor.h>
#include <goto-programs/goto_convert_class.h>
#include <goto-programs/remove_no_op.h>
#include <util/arith/arith_tools.h>
#include <util/lang/c_types.h>
#include <util/symtab/cprover_prefix.h>
#include <util/base/i2string.h>
#include <irep2/irep2_utils.h>
#include <util/message/message.h>
#include <util/message/format.h>
#include <util/base/prefix.h>
#include <util/symtab/replace_symbol.h>
#include <util/irep/std_expr.h>
#include <util/expr/type_byte_size.h>

Include dependency graph for goto_convert.cpp:

Functions
static irep_idt	destructor_entry_symbol (const codet &entry)
	The automatic object a destructor-stack entry cleans up: the symbol of a dead entry, or the this argument of a destructor call.
static void	collect_whole_reads (const expr2tc &e, std::set< irep_idt > &sources)
	The symbols e reads as whole objects: a member, an element or an address of one copies a part or none of it, so its temporary is still destroyed.
static bool	mentions_symbol (const exprt &e, const std::set< irep_idt > &ids)
static bool	reads_unwound_local (const exprt &e, const std::vector< codet > &stack, std::size_t from)
	Whether e reads a local whose dead entry sits on stack above from, i.e.
static std::set< irep_idt >	value_sources (const exprt &value, const goto_programt &sideeffects)
	The objects value is a bitwise copy of: the symbols it names and, transitively, those sideeffects assigns into them or into their parts (H{C(1)} lowers to tmp$2 = { .c=tmp$1 }).
static irep_idt	constructed_symbol (const expr2tc &code, const namespacet &ns)
	The object a constructor call builds: the symbol its this argument points to.
static bool	has_conditional_sideeffect (const exprt &expr, bool conditional=false)
	Whether a side effect sits under ?
static const exprt *	find_constructor_call (const exprt &e)
static void	elide_prvalue_temporary (exprt &initializer)
	A braced aggregate or a lambda's closure of the declared class initialises the variable itself ([dcl.init]/17.6.1): the temporary clang binds it to never exists, and copying out of it destroyed the value twice.
static void	collect_reference_member_temporaries (const exprt &init, std::set< irep_idt > &temporaries)
	The temporaries a braced aggregate initialiser binds to reference members, at any depth of nested aggregates.
static void	collect_atomic_reads (const exprt &expr, const namespacet &ns, std::map< irep_idt, typet > &out)
	Walks expr depth-first and inserts into out one entry per distinct _Atomic symbol that is actually read (i.e.

Function Documentation

collect_atomic_reads()

void collect_atomic_reads ( const exprt & expr, const namespacet & ns, std::map< irep_idt, typet > & out )

static

Walks expr depth-first and inserts into out one entry per distinct _Atomic symbol that is actually read (i.e.

not under address_of). The map key is the symbol identifier; the value is its type.

collect_reference_member_temporaries()

void collect_reference_member_temporaries ( const exprt & init, std::set< irep_idt > & temporaries )

static

The temporaries a braced aggregate initialiser binds to reference members, at any depth of nested aggregates.

collect_whole_reads()

void collect_whole_reads ( const expr2tc & e, std::set< irep_idt > & sources )

static

The symbols e reads as whole objects: a member, an element or an address of one copies a part or none of it, so its temporary is still destroyed.

constructed_symbol()

irep_idt constructed_symbol ( const expr2tc & code, const namespacet & ns )

static

The object a constructor call builds: the symbol its this argument points to.

Empty for any other call.

destructor_entry_symbol()

irep_idt destructor_entry_symbol ( const codet & entry )

static

The automatic object a destructor-stack entry cleans up: the symbol of a dead entry, or the this argument of a destructor call.

Empty if neither.

elide_prvalue_temporary()

void elide_prvalue_temporary ( exprt & initializer )

static

A braced aggregate or a lambda's closure of the declared class initialises the variable itself ([dcl.init]/17.6.1): the temporary clang binds it to never exists, and copying out of it destroyed the value twice.

find_constructor_call()

const exprt * find_constructor_call ( const exprt & e )

static

has_conditional_sideeffect()

bool has_conditional_sideeffect ( const exprt & expr, bool conditional = false )

static

Whether a side effect sits under ?

:, && or ||, so the temporaries it creates exist on one path only.

mentions_symbol()

bool mentions_symbol ( const exprt & e, const std::set< irep_idt > & ids )

static

reads_unwound_local()

bool reads_unwound_local ( const exprt & e, const std::vector< codet > & stack, std::size_t from )

static

Whether e reads a local whose dead entry sits on stack above from, i.e.

one that unwinding to from ends.

value_sources()

std::set< irep_idt > value_sources ( const exprt & value, const goto_programt & sideeffects )

static

The objects value is a bitwise copy of: the symbols it names and, transitively, those sideeffects assigns into them or into their parts (H{C(1)} lowers to tmp$2 = { .c=tmp$1 }).