ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
if_exprt Class Reference

#include <std_expr.h>

Inheritance diagram for if_exprt:
[legend]

Public Member Functions

 if_exprt (const exprt &cond, const exprt &t, const exprt &f)
 if_exprt ()
exprt & cond ()
const exprt & cond () const
exprt & true_case ()
const exprt & true_case () const
exprt & false_case ()
const exprt & false_case () const
Public Member Functions inherited from exprt
 exprt ()=default
 exprt (const irep_idt &_id)
 exprt (const irep_idt &_id, const typet &_type)
bool has_operands () const
operandst & operands ()
const operandst & operands () const
const irep_idt & value () const
void value (irep_idt val)
exprt & op0 ()
exprt & op1 ()
exprt & op2 ()
exprt & op3 ()
const exprt & op0 () const
const exprt & op1 () const
const exprt & op2 () const
const exprt & op3 () const
void reserve_operands (unsigned n)
void move_to_operands (exprt &expr)
void move_to_operands (exprt &e1, exprt &e2)
void move_to_operands (exprt &e1, exprt &e2, exprt &e3)
void copy_to_operands (const exprt &expr)
void copy_to_operands (const exprt &e1, const exprt &e2)
void copy_to_operands (const exprt &e1, const exprt &e2, const exprt &e3)
void make_typecast (const typet &_type)
void make_not ()
void make_true ()
void make_false ()
void make_bool (bool value)
void negate ()
bool sum (const exprt &expr)
bool mul (const exprt &expr)
bool subtract (const exprt &expr)
bool is_constant () const
bool is_true () const
bool is_false () const
bool is_zero () const
bool is_one () const
bool is_boolean () const
const locationt & find_location () const
const locationt & location () const
locationt & location ()
exprt & add_expr (const std::string &name)
const exprt & find_expr (const std::string &name) const
Public Member Functions inherited from irept
void dump () const
bool is_nil () const
bool is_not_nil () const
 irept (const irep_idt &_id)
 irept ()
 irept (const irept &irep)
irept & operator= (const irept &irep)
 ~irept ()
const irep_idt & id () const
const std::string & id_string () const
void id (const irep_idt &_data)
const irept & find (const irep_idt &name) const
irept & add (const irep_idt &name)
const std::string & get_string (const irep_idt &name) const
const irep_idt & get (const irep_idt &name) const
bool get_bool (const irep_idt &name) const
void set (const irep_idt &name, const irep_idt &value)
void set (const irep_idt &name, const long value)
void set (const irep_idt &name, const irept &irep)
void remove (const irep_idt &name)
void move_to_sub (irept &irep)
void move_to_named_sub (const irep_idt &name, irept &irep)
typet & type ()
const typet & type () const
bool is_identifier_set () const
const irep_idt & identifier () const
const irep_idt & width () const
const irep_idt & statement () const
const irep_idt & name () const
const irep_idt & component_name () const
const irep_idt & tag () const
const irep_idt & from () const
const irep_idt & file () const
const irep_idt & line () const
const irep_idt & function () const
const irept & function_irep () const
const irep_idt & column () const
const irep_idt & destination () const
const irep_idt & access () const
const irep_idt & base_name () const
const irep_idt & comment () const
const irep_idt & event () const
const irept & event_irep () const
const irep_idt & literal () const
const irep_idt & loopid () const
const irep_idt & mode () const
const irep_idt & module () const
const irep_idt & pretty_name () const
const irep_idt & derived_this_arg () const
bool base_ctor_derived () const
bool need_vptr_init () const
const irep_idt & property () const
const irep_idt & size () const
const irept & size_irep () const
const irep_idt & integer_bits () const
const irep_idt & to () const
const irep_idt & failed_symbol () const
const irep_idt & type_id () const
const irept & arguments () const
const irept & components () const
const irept & cmt_type () const
const irept & return_type () const
const irept & body () const
const irept & member_irep () const
const irept & labels_irep () const
const irept & bv () const
const irept & targets () const
const irept & variables () const
const irept & object_type () const
const irept & initializer () const
const irept & cmt_size () const
const irept & code () const
const irept & guard () const
const irept & location () const
const irept & declaration_type () const
const irept & decl_value () const
const irept & end_location () const
const irept & symvalue () const
const irept & cmt_location () const
const irept & decl_ident () const
bool is_decl_ident_set () const
const irept & elements () const
bool is_dynamic_set () const
bool dynamic () const
const irep_idt & cmt_base_name () const
const irep_idt & id_class () const
const irep_idt & cmt_identifier () const
const irep_idt & cformat () const
const irep_idt & member_name () const
 Owning class tag of a member function type, e.g.
const irep_idt & cpp_type () const
 Source-level spelling of a type, e.g.
const irep_idt & cmt_width () const
const irept & offsetof_type () const
bool axiom () const
bool cmt_constant () const
bool dfault () const
bool ellipsis () const
bool explict () const
bool file_local () const
bool hex_or_oct () const
bool hide () const
bool implicit () const
bool incomplete () const
bool initialization () const
bool inlined () const
bool invalid_object () const
bool is_parameter () const
bool is_expression () const
bool is_extern () const
bool is_macro () const
bool is_thread_local () const
bool is_type () const
bool lvalue () const
bool reference () const
bool restricted () const
bool static_lifetime () const
bool theorem () const
bool cmt_unsigned () const
bool user_provided () const
bool cmt_volatile () const
bool zero_initializer () const
void arguments (const irept &val)
void decl_ident (const irept &val)
void identifier (const irep_idt ident)
void statement (const irep_idt statm)
void comment (const irep_idt cmt)
void component_name (const irep_idt name)
void hex_or_oct (const irep_idt which)
void hex_or_oct (bool which)
void cmt_width (const irep_idt width)
void cmt_width (unsigned int width)
void width (const irep_idt width)
void width (unsigned int width)
void cmt_unsigned (const irep_idt val)
void cmt_unsigned (bool val)
void property (const irep_idt prop)
void cmt_base_name (const irep_idt name)
void name (const irep_idt val)
void cformat (const irep_idt val)
void member_name (const irep_idt val)
void cpp_type (const irep_idt val)
void remove_member_name ()
void flavor (const irep_idt val)
void function (const irep_idt val)
void size (const irep_idt val)
void size (const irept &val)
void user_provided (const irep_idt val)
void user_provided (bool val)
void destination (const irep_idt val)
void cmt_constant (const irep_idt val)
void cmt_constant (bool val)
void cmt_active (const irep_idt val)
void base_name (const irep_idt val)
void code (const irept &val)
void component (const irep_idt val)
void component (unsigned int val)
void dfault (bool val)
void dynamic (bool val)
void end_location (const irept &val)
void ellipsis (bool val)
void axiom (bool val)
void event (const irep_idt &val)
void failed_symbol (const irep_idt val)
void file (const irep_idt val)
void file_local (bool val)
void guard (const irept &val)
void hide (bool val)
void id_class (unsigned int val)
void cmt_identifier (const irep_idt val)
void implicit (bool val)
void incomplete (bool val)
void inlined (bool val)
void invalid_object (bool val)
void is_parameter (bool val)
void is_expression (bool val)
void is_extern (bool val)
void is_macro (bool val)
void is_thread_local (bool val)
void is_type (bool val)
void label (const irep_idt &val)
void lhs (bool val)
void line (const irep_idt &val)
void line (unsigned int val)
void location (const irept &val)
void lvalue (bool val)
void mode (const irep_idt &val)
void module (const irep_idt &val)
void object_type (const irept &val)
void pretty_name (const irep_idt &val)
void derived_this_arg (const irep_idt &val)
void base_ctor_derived (bool val)
void need_vptr_init (bool val)
void restricted (bool val)
void cmt_size (const irept &val)
void static_lifetime (bool val)
void tag (const irep_idt &val)
void theorem (bool val)
void cmt_type (const irept &val)
void type_id (unsigned int val)
void cmt_volatile (bool val)
void zero_initializer (bool val)
void components (const irept &val)
void offsetof_type (const irept &val)
void declaration_type (const irept &val)
void bv (const irept &val)
void initializer (const irept &val)
void labels (const irept &val)
void symvalue (const irept &val)
void member_irep (const irept &val)
void return_type (const irept &val)
void variables (const irept &val)
void targets (const irept &val)
bool is_address_of () const
bool is_and () const
bool is_or () const
bool is_array () const
bool is_bool () const
bool is_code () const
bool is_function_call () const
bool is_constant () const
bool is_dereference () const
bool is_empty () const
bool is_fixedbv () const
bool is_floatbv () const
bool is_incomplete_array () const
bool is_index () const
bool is_member () const
bool is_not () const
bool is_notequal () const
bool is_pointer () const
bool is_signedbv () const
bool is_struct () const
bool is_symbol () const
bool is_typecast () const
bool is_union () const
bool is_unsignedbv () const
bool is_vector () const
std::string to_string () const
void swap (irept &irep)
int compare (const irept &i) const
void clear ()
void make_nil ()
subt & get_sub ()
const subt & get_sub () const
named_subt & get_named_sub ()
const named_subt & get_named_sub () const
named_subt & get_comments ()
const named_subt & get_comments () const
size_t hash () const
size_t full_hash () const
std::string pretty (unsigned indent=0) const

Additional Inherited Members

Public Types inherited from exprt
typedef std::vector< exprt > operandst
Public Types inherited from irept
typedef std::vector< irept > subt
typedef std::map< irep_idt, irept > named_subt
Static Public Attributes inherited from exprt
static irep_idt trans = irep_idt("trans")
static irep_idt symbol = irep_idt("symbol")
static irep_idt plus = irep_idt("+")
static irep_idt minus = irep_idt("-")
static irep_idt mult = irep_idt("*")
static irep_idt div = irep_idt("/")
static irep_idt mod = irep_idt("mod")
static irep_idt equality = irep_idt("=")
static irep_idt notequal = irep_idt("notequal")
static irep_idt index = irep_idt("index")
static irep_idt arrayof = irep_idt("array_of")
static irep_idt objdesc = irep_idt("object_descriptor")
static irep_idt dynobj = irep_idt("dynamic_object")
static irep_idt typecast = irep_idt("typecast")
static irep_idt implies = irep_idt("=>")
static irep_idt i_and = irep_idt("and")
static irep_idt i_xor = irep_idt("xor")
static irep_idt i_or = irep_idt("or")
static irep_idt i_not = irep_idt("not")
static irep_idt addrof = irep_idt("address_of")
static irep_idt deref = irep_idt("dereference")
static irep_idt i_if = irep_idt("if")
static irep_idt with = irep_idt("with")
static irep_idt member = irep_idt("member")
static irep_idt member_ref = irep_idt("member_ref")
static irep_idt ptr_mem = irep_idt("ptr_mem")
static irep_idt isnan = irep_idt("isnan")
static irep_idt ieee_floateq = irep_idt("ieee_float_equal")
static irep_idt i_type = irep_idt("type")
static irep_idt constant = irep_idt("constant")
static irep_idt i_true = irep_idt("true")
static irep_idt i_false = irep_idt("false")
static irep_idt i_lt = irep_idt("<")
static irep_idt i_gt = irep_idt(">")
static irep_idt i_le = irep_idt("<=")
static irep_idt i_ge = irep_idt(">=")
static irep_idt i_cmp_three_way = irep_idt("<=>")
static irep_idt i_bitand = irep_idt("bitand")
static irep_idt i_bitor = irep_idt("bitor")
static irep_idt i_bitxor = irep_idt("bitxor")
static irep_idt i_bitnot = irep_idt("bitnot")
static irep_idt i_ashr = irep_idt("ashr")
static irep_idt i_lshr = irep_idt("lshr")
static irep_idt i_shl = irep_idt("shl")
static irep_idt abs = irep_idt("abs")
static irep_idt argument = irep_idt("argument")
static irep_idt a_value = irep_idt("value")
Static Public Attributes inherited from irept
static const irep_idt s_type = irep_idt("type")
static const irep_idt s_arguments = irep_idt("arguments")
static const irep_idt s_components = irep_idt("components")
static const irep_idt s_return_type = irep_idt("return_type")
static const irep_idt s_body = irep_idt("body")
static const irep_idt s_member = irep_idt("member")
static const irep_idt s_labels = irep_idt("labels")
static const irep_idt s_bv = irep_idt("bv")
static const irep_idt s_targets = irep_idt("targets")
static const irep_idt s_variables = irep_idt("variables")
static const irep_idt s_initializer = irep_idt("initializer")
static const irep_idt s_declaration_type = irep_idt("declaration_type")
static const irep_idt s_decl_value = irep_idt("decl_value")
static const irep_idt s_symvalue = irep_idt("symvalue")
static const irep_idt s_cmt_location = irep_idt("#location")
static const irep_idt s_decl_ident = irep_idt("decl_ident")
static const irep_idt s_elements = irep_idt("elements")
static const irep_idt s_offsetof_type = irep_idt("offsetof_type")
static const irep_idt a_width = irep_idt("width")
static const irep_idt a_name = irep_idt("name")
static const irep_idt a_statement = irep_idt("statement")
static const irep_idt a_identifier = irep_idt("identifier")
static const irep_idt a_comp_name = irep_idt("component_name")
static const irep_idt a_tag = irep_idt("tag")
static const irep_idt a_from = irep_idt("from")
static const irep_idt a_file = irep_idt("file")
static const irep_idt a_line = irep_idt("line")
static const irep_idt a_function = irep_idt("function")
static const irep_idt a_column = irep_idt("column")
static const irep_idt a_access = irep_idt("access")
static const irep_idt a_destination = irep_idt("destination")
static const irep_idt a_base_name = irep_idt("base_name")
static const irep_idt a_comment = irep_idt("comment")
static const irep_idt a_event = irep_idt("event")
static const irep_idt a_literal = irep_idt("literal")
static const irep_idt a_loopid = irep_idt("loop-id")
static const irep_idt a_mode = irep_idt("mode")
static const irep_idt a_module = irep_idt("module")
static const irep_idt a_pretty_name = irep_idt("pretty_name")
static const irep_idt a_property = irep_idt("property")
static const irep_idt a_size = irep_idt("size")
static const irep_idt a_integer_bits = irep_idt("integer_bits")
static const irep_idt a_to = irep_idt("to")
static const irep_idt a_failed_symbol = irep_idt("#failed_symbol")
static const irep_idt a_dynamic = irep_idt("#dynamic")
static const irep_idt a_cmt_base_name = irep_idt("#base_name")
static const irep_idt a_id_class = irep_idt("#id_class")
static const irep_idt a_cmt_identifier = irep_idt("#identifier")
static const irep_idt a_cformat = irep_idt("#cformat")
static const irep_idt a_cmt_width = irep_idt("#width")
static const irep_idt a_axiom = irep_idt("axiom")
static const irep_idt a_member_name = irep_idt("#member_name")
static const irep_idt a_cpp_type = irep_idt("#cpp_type")
static const irep_idt a_cmt_constant = irep_idt("#constant")
static const irep_idt a_default = irep_idt("default")
static const irep_idt a_ellipsis = irep_idt("ellipsis")
static const irep_idt a_explicit = irep_idt("explicit")
static const irep_idt a_file_local = irep_idt("file_local")
static const irep_idt a_hex_or_oct = irep_idt("#hex_or_oct")
static const irep_idt a_hide = irep_idt("#hide")
static const irep_idt a_implicit = irep_idt("#implicit")
static const irep_idt a_incomplete = irep_idt("#incomplete")
static const irep_idt a_initialization = irep_idt("initialization")
static const irep_idt a_inlined = irep_idt("#inlined")
static const irep_idt a_invalid_object = irep_idt("#invalid_object")
static const irep_idt a_is_parameter = irep_idt("is_parameter")
static const irep_idt a_is_expression = irep_idt("#is_expression")
static const irep_idt a_is_extern = irep_idt("is_extern")
static const irep_idt a_is_macro = irep_idt("is_macro")
static const irep_idt a_is_thread_local = irep_idt("is_thread_local")
static const irep_idt a_is_type = irep_idt("is_type")
static const irep_idt a_lvalue = irep_idt("lvalue")
static const irep_idt a_reference = irep_idt("#reference")
static const irep_idt a_static_lifetime = irep_idt("static_lifetime")
static const irep_idt a_theorem = irep_idt("theorem")
static const irep_idt a_cmt_unsigned = irep_idt("#unsigned")
static const irep_idt a_user_provided = irep_idt("user-provided")
static const irep_idt a_cmt_volatile = irep_idt("#volatile")
static const irep_idt a_zero_initializer = irep_idt("#zero_initializer")
static const irep_idt a_restricted = irep_idt("#restricted")
static const irep_idt a_flavor = irep_idt("flavor")
static const irep_idt a_cmt_active = irep_idt("#active")
static const irep_idt a_code = irep_idt("code")
static const irep_idt a_component = irep_idt("component")
static const irep_idt a_end_location = irep_idt("#end_location")
static const irep_idt a_guard = irep_idt("guard")
static const irep_idt a_label = irep_idt("label")
static const irep_idt a_lhs = irep_idt("lhs")
static const irep_idt a_location = irep_idt("location")
static const irep_idt a_object_type = irep_idt("object_type")
static const irep_idt a_cmt_size = irep_idt("#size")
static const irep_idt a_cmt
static const irep_idt a_type_id = irep_idt("typeid")
static const irep_idt a_cmt_type = irep_idt("#type")
static const irep_idt a_derived_this_arg = irep_idt("#derived_this_arg")
static const irep_idt a_base_ctor_derived = irep_idt("#base_ctor_derived")
static const irep_idt a_need_vptr_init = irep_idt("#need_vptr_init")
static const irep_idt id_address_of = irep_idt("address_of")
static const irep_idt id_and = irep_idt("and")
static const irep_idt id_or = irep_idt("or")
static const irep_idt id_array = irep_idt("array")
static const irep_idt id_bool = irep_idt("bool")
static const irep_idt id_code = irep_idt("code")
static const irep_idt id_constant = irep_idt("constant")
static const irep_idt id_dereference = irep_idt("dereference")
static const irep_idt id_empty = irep_idt("empty")
static const irep_idt id_fixedbv = irep_idt("fixedbv")
static const irep_idt id_floatbv = irep_idt("floatbv")
static const irep_idt id_incomplete_array = irep_idt("incomplete_array")
static const irep_idt id_index = irep_idt("index")
static const irep_idt id_member = irep_idt("member")
static const irep_idt id_not = irep_idt("not")
static const irep_idt id_notequal = irep_idt("notequal")
static const irep_idt id_pointer = irep_idt("pointer")
static const irep_idt id_signedbv = irep_idt("signedbv")
static const irep_idt id_struct = irep_idt("struct")
static const irep_idt id_symbol = irep_idt("symbol")
static const irep_idt id_typecast = irep_idt("typecast")
static const irep_idt id_union = irep_idt("union")
static const irep_idt id_unsignedbv = irep_idt("unsignedbv")
static const irep_idt id_vector = irep_idt("vector")
Protected Member Functions inherited from irept
void remove_ref (dt *old_data)
const dt & read () const
dt & write ()
void detatch ()
Static Protected Member Functions inherited from irept
static bool is_comment (const irep_idt &name)
Protected Attributes inherited from irept
dt * data
Static Protected Attributes inherited from exprt
static irep_idt o_operands = irep_idt("operands")
static irep_idt o_location = irep_idt("#location")

Constructor & Destructor Documentation

◆ if_exprt() [1/2]

if_exprt::if_exprt ( const exprt & cond,
const exprt & t,
const exprt & f )
inline

◆ if_exprt() [2/2]

if_exprt::if_exprt ( )
inline

Member Function Documentation

◆ cond() [1/2]

exprt & if_exprt::cond ( )
inline

◆ cond() [2/2]

const exprt & if_exprt::cond ( ) const
inline

◆ false_case() [1/2]

exprt & if_exprt::false_case ( )
inline

◆ false_case() [2/2]

const exprt & if_exprt::false_case ( ) const
inline

◆ true_case() [1/2]

exprt & if_exprt::true_case ( )
inline

◆ true_case() [2/2]

const exprt & if_exprt::true_case ( ) const
inline

The documentation for this class was generated from the following file: