21{

26 {

28 vm,

30 "nil array size must be exactly nil");

31 }

32}

48 const irep_idt &component_name) const

49{

50 std::size_t number=0;

51

53 {

54 if(c.get_name() == component_name)

55 return number;

56

57 number++;

58 }

59

61}

65 const irep_idt &component_name) const

66{

68 {

69 if(c.get_name() == component_name)

70 return c;

71 }

72

74}

78{

81 return c.type();

82}

106{

107 for(const auto &b : bases())

108 {

110 return b;

111 }

112 return {};

113}

120{

123

126 return false;

127

128 componentst::const_iterator

130

132 {

133 if(ot_it->type() != tt_c.type() || ot_it->get_name() != tt_c.get_name())

134 {

135 return false;

136 }

137

139 }

140

141 return true;

142}

169{

170 return get_from() <= singleton && singleton <= get_to();

171}

215 const typet &type,

217{

218

219

222 {

225 {

227 return true;

228 }

229 }

230 return false;

231 };

232

233

234

235

236

237

238

239

241 return true;

242

243

244

245

246

247

250

251

252

253

254

255

257 {

260 }

262 {

265 }

266

267

268

269

270

271

273 {

276 }

277

278 return false;

279}

286{

288 size() = std::move(_size);

289}

292{

293

294

299 else

301}

bitvector_typet c_index_type()

const union_tag_typet & to_union_tag_type(const typet &type)

Cast a typet to a union_tag_typet.

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)

typet index_type() const

The type of the index expressions into any instance of this type.

std::size_t width() const

A constant literal expression.

dstringt has one field, an unsigned integer no which is an index into a static table of strings.

Base class for all expressions.

typet & type()

Return the type of the expression.

bool get_bool(const irep_idt &name) const

std::size_t get_size_t(const irep_idt &name) const

const irept & find(const irep_idt &name) const

void set(const irep_idt &name, const irep_idt &value)

const irep_idt & id() const

irept & add(const irep_idt &name)

const std::string & get_string(const irep_idt &name) const

const union_typet & follow_tag(const union_tag_typet &) const

Follow type tag of union type.

A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...

void set_to(const mp_integer &to)

constant_exprt zero_expr() const

void set_from(const mp_integer &_from)

mp_integer get_to() const

bool includes(const mp_integer &) const

constant_exprt one_expr() const

mp_integer get_from() const

A struct tag type, i.e., struct_typet with an identifier.

Base class or struct that a class or struct inherits from.

baset(struct_tag_typet base)

struct_tag_typet & type()

Structure type, corresponds to C style structs.

const basest & bases() const

Get the collection of base classes/structs.

std::optional< baset > get_base(const irep_idt &id) const

Return the base with the given name, if exists.

bool is_prefix_of(const struct_typet &other) const

Returns true if the struct is a prefix of other, i.e., if this struct has n components then the compo...

void add_base(const struct_tag_typet &base)

Add a base class/struct.

const typet & component_type(const irep_idt &component_name) const

const componentst & components() const

const componentt & get_component(const irep_idt &component_name) const

Get the reference to a component with given name.

std::size_t component_number(const irep_idt &component_name) const

Return the sequence number of the component with given name.

std::vector< componentt > componentst

Type with a single subtype.

static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)

The type of an expression, extends irept.

vector_typet(typet index_type, typet element_type, constant_exprt size)

const constant_exprt & size() const

typet & index_type_nonconst()

The type of any index expression into an instance of this type.

typet index_type() const

The type of any index expression into an instance of this type.

const irept & get_nil_irep()

const mp_integer string2integer(const std::string &n, unsigned base)

const std::string integer2string(const mp_integer &n, unsigned base)

bool is_reference(const typet &type)

Returns true if the type is a reference.

bool is_rvalue_reference(const typet &type)

Returns if the type is an R value reference.

#define CHECK_RETURN(CONDITION)

#define UNREACHABLE

This should be used to mark dead code.

#define PRECONDITION(CONDITION)

auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())

API to expression classes.

bool is_constant_or_has_constant_components(const typet &type, const namespacet &ns)

Identify whether a given type is constant itself or contains constant components.

const struct_tag_typet & to_struct_tag_type(const typet &type)

Cast a typet to a struct_tag_typet.

const struct_union_typet & to_struct_union_type(const typet &type)

Cast a typet to a struct_union_typet.

const type_with_subtypet & to_type_with_subtype(const typet &type)

#define DATA_CHECK(vm, condition, message)

This macro takes a condition which denotes a well-formedness criterion on goto programs,...