24{

25public:

31

39

47

48

54

55

61

66

74};

121{

122public:

128

143};

181{

182public:

191

200

206

211

216

222

227

232};

241{

242 validate_operands(value, 2, "Object descriptor must have two operands");

243}

253{

258 return ret;

259}

263{

267 return ret;

268}

272{

273public:

282

284

286

291

296};

316{

321 return ret;

322}

326{

330 return ret;

331}

335{

336public:

341

346

351};

360{

361 validate_operands(value, 1, "is_dynamic_object must have one operand");

362}

366{

369 expr.operands().size() == 1, "is_dynamic_object must have one operand");

371}

376{

379 expr.operands().size() == 1, "is_dynamic_object must have one operand");

381}

387{

388public:

401

406

411

416

417

419};

428{

429 validate_operands(value, 3, "pointer_in_range must have three operands");

430}

433{

436 expr.operands().size() == 3, "pointer_in_range must have three operands");

438}

443{

446 expr.operands().size() == 3, "pointer_in_range must have three operands");

448}

453{

454public:

474

479

484

489

494

499

500

502};

511{

513 value, 5, "prophecy_pointer_in_range must have five operands");

514}

518{

522 "prophecy_pointer_in_range must have five operands");

524}

530{

534 "prophecy_pointer_in_range must have five operands");

536}

540{

541public:

543

548

553

558};

578{

582 return ret;

583}

587{

591 return ret;

592}

596{

597public:

599

601

606

611

616

622

624};

644{

649 return ret;

650}

654{

658 return ret;

659}

664{

665public:

672

677

682

687

692

698

703

708};

728{

733 return ret;

734}

738{

742 return ret;

743}

748{

749public:

754

759

764

769

775

780

785

790

795};

815{

820 return ret;

821}

825{

829 return ret;

830}

834{

835public:

836

841

846

851

856

866

868 const exprt &expr,

871};

891{

895 return ret;

896}

900{

904 return ret;

905}

920{

921public:

926

931

936};

950{

955 return ret;

956}

980{

984 return ret;

985}

1009{

1013 return ret;

1014}

1019{

1020public:

1036

1046

1051

1056

1061

1066

1071

1076

1080};

1096{

1102 return ret;

1103}

1107{

1108public:

1122

1131};

1145{

1150 return ret;

1151}

1155{

1156public:

1170

1179};

1193{

1198 return ret;

1199}

1210{

1211public:

1219

1224

1229

1234

1239};

1248{

1250 value, 1, "Annotated pointer constant must have one operand");

1251}

1261{

1266 return ret;

1267}

1272{

1277 return ret;

1278}

1282{

1283public:

1288

1293

1298};

1307{

1308 validate_operands(value, 1, "pointer_offset must have one operand");

1311 "pointer_offset must have pointer-typed operand");

1312}

1321{

1326 return ret;

1327}

1331{

1335 return ret;

1336}

1340{

1341public:

1346

1351

1356};

1365{

1366 validate_operands(value, 1, "pointer_object must have one operand");

1369 "pointer_object must have pointer-typed operand");

1370}

1379{

1384 return ret;

1385}

1389{

1393 return ret;

1394}

1399{

1400public:

1405

1410

1415};

1424{

1428 return ret;

1429}

1433{

1437 return ret;

1438}

1447{

1448 validate_operands(value, 1, "Object size expression must have one operand.");

1451 "Object size expression must have pointer typed operand.");

1452}

1458{

1459public:

1465

1470

1475};

1495{

1499 return ret;

1500}

1504{

1508 return ret;

1509}

1516{

1517public:

1523

1528

1533};

1553{

1557 return ret;

1558}

1562{

1566 return ret;

1567}

1572{

1573public:

1579

1584

1589};

1609{

1613 return ret;

1614}

1618{

1622 return ret;

1623}

1628{

1629public:

1635

1640

1645};

1654{

1655 validate_operands(value, 1, "writeable_object must have one operand");

1656}

1665{

1670 return ret;

1671}

1675{

1679 return ret;

1680}

1684{

1685public:

1690

1699};

1718{

1722 return ret;

1723}

1727{

1731 return ret;

1732}

const T & as_const(T &value)

Return a reference to the same object but ensures the type is const.

Pre-defined bitvector types.

reference_typet reference_type(const typet &subtype)

Operator to return the address of an object.

const exprt & object() const

address_of_exprt(exprt op, pointer_typet _type)

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

Pointer-typed bitvector constant annotated with the pointer expression that the bitvector is the nume...

const irep_idt & get_value() const

void set_value(const irep_idt &value)

const exprt & symbolic_pointer() const

annotated_pointer_constant_exprt(const irep_idt &_value, const exprt &_pointer)

exprt & symbolic_pointer()

A base class for binary expressions.

A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...

Base class of fixed-width bit-vector types.

std::size_t get_width() const

std::size_t width() const

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

A constant literal expression.

An expression, akin to ISO C's strlen, that denotes the length of a zero-terminated string that start...

cstrlen_exprt(exprt address, typet type)

const exprt & address() const

Operator to dereference a pointer.

static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)

dereference_exprt(const exprt &op)

const exprt & pointer() const

static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)

Check that the dereference expression has the right number of operands, refers to something with a po...

dereference_exprt(exprt op, typet type)

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

Representation of heap-allocated objects.

unsigned int get_instance() const

void set_instance(unsigned int instance)

const exprt & valid() const

dynamic_object_exprt(typet type)

Operator to return the address of an array element relative to a base address.

const typet & element_type() const

returns the type of the array element whose address is represented

const exprt & index() const

const pointer_typet & type() const

const exprt & base() const

Base class for all expressions.

Base class for all expressions.

std::vector< exprt > operandst

typet & type()

Return the type of the expression.

Operator to return the address of a field relative to a base address.

const typet & field_type() const

returns the type of the field whose address is represented

const exprt & base() const

const irep_idt & component_name() const

const typet & compound_type() const

const pointer_typet & type() const

bool get_bool(const irep_idt &name) const

const irep_idt & get(const irep_idt &name) const

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

const irep_idt & id() const

A predicate that indicates that a zero-terminated string starts at the given address.

const exprt & address() const

is_cstring_exprt(exprt address)

Evaluates to true if the operand is a pointer to a dynamic object.

is_dynamic_object_exprt(const exprt &op)

const exprt & address() const

A predicate that indicates that the object pointed to is live.

const exprt & pointer() const

live_object_exprt(exprt pointer)

A base class for multi-ary expressions Associativity is not specified.

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

The null pointer constant.

null_pointer_exprt(pointer_typet type)

An expression without operands.

Operator to return the address of an object.

const pointer_typet & type() const

symbol_exprt object_expr() const

irep_idt object_identifier() const

const typet & object_type() const

returns the type of the object whose address is represented

Split an expression into a base object and a (byte) offset.

object_descriptor_exprt()

const exprt & root_object() const

object_descriptor_exprt(exprt _object)

const exprt & offset() const

void build(const exprt &expr, const namespacet &ns)

Given an expression expr, attempt to find the underlying object it represents by skipping over type c...

const exprt & object() const

Expression for finding the size (in bytes) of the object a pointer points to.

object_size_exprt(exprt pointer, typet type)

const exprt & pointer() const

pointer_in_range(a, b, c) evaluates to true iff same_object(a, b, c) ∧ r_ok(a, offset(c)-offset(a)) ∧...

pointer_in_range_exprt(exprt a, exprt b, exprt c)

const exprt & upper_bound() const

const exprt & lower_bound() const

const exprt & pointer() const

A numerical identifier for the object a pointer points to.

const exprt & pointer() const

pointer_object_exprt(exprt pointer, typet type)

The offset (in bytes) of a pointer relative to the object.

pointer_offset_exprt(exprt pointer, typet type)

const exprt & pointer() const

The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...

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

signedbv_typet difference_type() const

const typet & base_type() const

The type of the data what we point to.

typet & base_type()

The type of the data what we point to.

pointer_typet(typet _base_type, std::size_t width)

const typet & subtype() const

pointer_in_range (see pointer_in_range_exprt) with prophecy expressions to encode whether a pointer r...

const exprt & upper_bound() const

const exprt & dead_ptr() const

const exprt & lower_bound() const

const exprt & pointer() const

const exprt & deallocated_ptr() const

exprt lower(const namespacet &ns) const

prophecy_pointer_in_range_exprt(exprt a, exprt b, exprt c, exprt is_deallocated, exprt is_dead)

A predicate that indicates that an address range is ok to read.

prophecy_r_ok_exprt(exprt pointer, exprt size)

prophecy_r_ok_exprt(exprt pointer, exprt size, exprt is_deallocated, exprt is_dead)

A base class for a predicate that indicates that an address range is ok to read or write or both.

prophecy_r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size, exprt is_deallocated, exprt is_dead)

const exprt & deallocated_ptr() const

exprt lower(const namespacet &ns) const

Lower an r_or_w_ok_exprt to arithmetic and logic expressions.

const exprt & dead_ptr() const

const exprt & pointer() const

prophecy_r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size)

exprt & deallocated_ptr()

const exprt & size() const

A predicate that indicates that an address range is ok to write.

prophecy_w_ok_exprt(exprt pointer, exprt size)

prophecy_w_ok_exprt(exprt pointer, exprt size, exprt is_deallocated, exprt is_dead)

A predicate that indicates that an address range is ok to read.

r_ok_exprt(exprt pointer, exprt size)

A base class for a predicate that indicates that an address range is ok to read or write or both.

const exprt & size() const

r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size)

const exprt & pointer() const

reference_typet(typet _subtype, std::size_t _width)

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

A predicate that indicates that the objects pointed to are distinct.

separate_exprt(exprt::operandst __operands)

separate_exprt(exprt __op0, exprt __op1)

Fixed-width bit-vector with two's complement interpretation.

Expression to hold a symbol (variable)

An expression with three operands.

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

The type of an expression, extends irept.

Generic base class for unary expressions.

A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...

A predicate that indicates that an address range is ok to write.

w_ok_exprt(exprt pointer, exprt size)

A predicate that indicates that the object pointed to is writeable.

writeable_object_exprt(exprt pointer)

const exprt & pointer() const

void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)

const live_object_exprt & to_live_object_expr(const exprt &expr)

Cast an exprt to a live_object_exprt.

bool can_cast_expr< separate_exprt >(const exprt &base)

const separate_exprt & to_separate_expr(const exprt &expr)

Cast an exprt to a separate_exprt.

void validate_expr(const object_descriptor_exprt &value)

bool can_cast_type< reference_typet >(const typet &type)

Check whether a reference to a typet is a reference_typet.

const prophecy_r_ok_exprt & to_prophecy_r_ok_expr(const exprt &expr)

bool can_cast_expr< field_address_exprt >(const exprt &expr)

bool is_void_pointer(const typet &type)

This method tests, if the given typet is a pointer of type void.

bool can_cast_type< pointer_typet >(const typet &type)

Check whether a reference to a typet is a pointer_typet.

const prophecy_w_ok_exprt & to_prophecy_w_ok_expr(const exprt &expr)

const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)

Cast an exprt to an object_descriptor_exprt.

bool can_cast_expr< prophecy_w_ok_exprt >(const exprt &base)

bool can_cast_expr< live_object_exprt >(const exprt &base)

bool is_reference(const typet &type)

Returns true if the type is a reference.

const r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)

const element_address_exprt & to_element_address_expr(const exprt &expr)

Cast an exprt to an element_address_exprt.

const annotated_pointer_constant_exprt & to_annotated_pointer_constant_expr(const exprt &expr)

Cast an exprt to an annotated_pointer_constant_exprt.

bool can_cast_expr< dynamic_object_exprt >(const exprt &base)

const object_address_exprt & to_object_address_expr(const exprt &expr)

Cast an exprt to an object_address_exprt.

const cstrlen_exprt & to_cstrlen_expr(const exprt &expr)

Cast an exprt to a cstrlen_exprt.

bool can_cast_expr< pointer_in_range_exprt >(const exprt &base)

bool can_cast_expr< prophecy_pointer_in_range_exprt >(const exprt &base)

bool can_cast_expr< dereference_exprt >(const exprt &base)

bool is_rvalue_reference(const typet &type)

Returns if the type is an R value reference.

bool can_cast_expr< is_dynamic_object_exprt >(const exprt &base)

const writeable_object_exprt & to_writeable_object_expr(const exprt &expr)

Cast an exprt to a writeable_object_exprt.

bool can_cast_expr< cstrlen_exprt >(const exprt &base)

const reference_typet & to_reference_type(const typet &type)

Cast a typet to a reference_typet.

bool can_cast_expr< object_address_exprt >(const exprt &base)

const prophecy_pointer_in_range_exprt & to_prophecy_pointer_in_range_expr(const exprt &expr)

bool can_cast_expr< object_size_exprt >(const exprt &base)

bool can_cast_expr< is_cstring_exprt >(const exprt &base)

bool can_cast_expr< annotated_pointer_constant_exprt >(const exprt &base)

const pointer_in_range_exprt & to_pointer_in_range_expr(const exprt &expr)

bool can_cast_expr< address_of_exprt >(const exprt &base)

const address_of_exprt & to_address_of_expr(const exprt &expr)

Cast an exprt to an address_of_exprt.

bool can_cast_expr< pointer_offset_exprt >(const exprt &base)

const pointer_typet & to_pointer_type(const typet &type)

Cast a typet to a pointer_typet.

bool can_cast_expr< w_ok_exprt >(const exprt &base)

const w_ok_exprt & to_w_ok_expr(const exprt &expr)

const prophecy_r_or_w_ok_exprt & to_prophecy_r_or_w_ok_expr(const exprt &expr)

const r_ok_exprt & to_r_ok_expr(const exprt &expr)

bool can_cast_expr< element_address_exprt >(const exprt &expr)

bool can_cast_expr< r_ok_exprt >(const exprt &base)

const dereference_exprt & to_dereference_expr(const exprt &expr)

Cast an exprt to a dereference_exprt.

const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)

Cast an exprt to a pointer_offset_exprt.

const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)

Cast an exprt to a pointer_object_exprt.

const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)

Cast an exprt to a dynamic_object_exprt.

const is_cstring_exprt & to_is_cstring_expr(const exprt &expr)

Cast an exprt to a is_cstring_exprt.

bool can_cast_expr< r_or_w_ok_exprt >(const exprt &base)

const field_address_exprt & to_field_address_expr(const exprt &expr)

Cast an exprt to an field_address_exprt.

bool can_cast_expr< object_descriptor_exprt >(const exprt &base)

const object_size_exprt & to_object_size_expr(const exprt &expr)

Cast an exprt to a object_size_exprt.

const is_dynamic_object_exprt & to_is_dynamic_object_expr(const exprt &expr)

bool can_cast_expr< prophecy_r_or_w_ok_exprt >(const exprt &base)

bool can_cast_expr< writeable_object_exprt >(const exprt &base)

bool can_cast_expr< pointer_object_exprt >(const exprt &base)

bool can_cast_expr< prophecy_r_ok_exprt >(const exprt &base)

#define DATA_INVARIANT(CONDITION, REASON)

This condition should be used to document that assumptions that are made on goto_functions,...

#define PRECONDITION(CONDITION)

API to expression classes.

#define DATA_CHECK(vm, condition, message)

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