27{

29 return val.find_first_not_of('0')==std::string::npos;

30}

53{

56 else

57 return false;

58}

61{

64 else

65 return true;

66}

69{

70 if(rhs == 0)

71 {

73

75 {

77 }

79 {

81 }

83 {

85 }

87 {

92 }

93 else if(

96 {

98 }

100 {

102 }

104 {

106 }

108 {

109 return *this == nullptr;

110 }

111 else

112 return false;

113 }

114 else if(rhs == 1)

115 {

117

119 {

121 }

123 {

125 }

127 {

129 }

131 {

136 }

137 else if(

140 {

145 }

147 {

151 return one == fixedbvt{*this};

152 }

154 {

156 }

157 else

158 return false;

159 }

160 else

162}

165{

167 return !(*this == rhs);

168}

171{

173 return false;

174

176 return true;

177

178

179

182 "front-end should use ID_NULL");

183 return false;

184}

211{

213

215

217 vm,

219 "bitvector constant must have a non-empty value");

220

222 vm,

228 std::string::npos,

229 "negative bitvector constant must use two's complement");

230

232 vm,

237 "bitvector constant must not have leading zeros");

238}

241{

242 if(op.empty())

244 else if(op.size()==1)

245 return op.front();

246 else

247 {

249 }

250}

253{

255 if(b.is_constant())

256 {

259 return a;

260 }

261 if(a.is_constant())

262 {

265 return b;

266 }

268 {

269 b.add_to_operands(std::move(a));

270 return b;

271 }

272 return and_exprt{std::move(a), std::move(b)};

273}

276{

277 if(op.empty())

279 else if(op.size()==1)

280 return op.front();

281 else if(op.size() == 2)

283 else

284 {

286 }

287}

293{

294 static_assert(

295 std::is_base_of<struct_exprt, T>::value, "T must be a struct_exprt.");

300 const auto index = struct_type.component_number(name);

303 "component matching index should exist");

305}

309{

310 return ::component(*this, name, ns);

311}

316{

317 return ::component(*this, name, ns);

318}

328 const exprt &expr,

331{

333

335

342 vm,

344 "member must address a struct, union or compatible type");

345

348

350 vm,

353 "' must exist on addressed type");

354

356 vm,

358 "member expression's type must match the addressed struct or union "

359 "component");

360}

363{

365

367

369 vm,

371 "number of variables must match number of values");

372

373 for(const auto &binding :

375 {

377 vm,

379 "let binding symbols must be symbols");

380

382 vm,

384 "let bindings must be type consistent");

385 }

386}

389{

392

394 exprt *dest = &result;

395

397 {

399

401 {

403 }

405 {

406

407

408 }

409 else

411

412 *dest = tmp;

414 }

415

416 return result;

417}

420{

421

424

425 std::map<symbol_exprt, exprt> value_map;

426

427 for(std::size_t i = 0; i < variables.size(); i++)

428 {

429

431 value_map[variables[i]] = values[i];

432 }

433

434

436

437 for(std::size_t i = 0; i < variables.size(); i++)

439

440

442

445 else

446 return where();

447}

450{

451 std::vector<exprt> values;

452 values.reserve(new_variables.size());

453 for(const auto &new_variable : new_variables)

454 values.push_back(new_variable);

456}

459{

461 operands().size() % 2 == 0, "cond must have even number of operands");

462

464

466

467

468 for(std::size_t i = operands.size(); i != 0; i -= 2)

469 {

471 i >= 2,

472 "since the number of operands is even if i is nonzero it must be "

473 "greater than two");

474

477

479 result = value;

480 else

481 result = if_exprt{cond, value, std::move(result)};

482 }

483

484 return result;

485}

const fixedbv_typet & to_fixedbv_type(const typet &type)

Cast a typet to a fixedbv_typet.

const bitvector_typet & to_bitvector_type(const typet &type)

Cast a typet to a bitvector_typet.

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

Boolean AND All operands must be boolean, and the result is always boolean.

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

exprt instantiate(const exprt::operandst &) const

substitute free occurrences of the variables in where() by the given values

std::vector< symbol_exprt > variablest

struct configt::ansi_ct ansi_c

const irep_idt & get_value() const

bool operator!=(bool rhs) const

Return whether the expression lhs is not a constant of Boolean type or is not representing the Boolea...

bool value_is_zero_string() const

bool operator==(bool rhs) const

Return whether the expression lhs is a constant of Boolean type that is representing the Boolean valu...

bool is_null_pointer() const

Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...

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

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

Base class for all expressions.

std::vector< exprt > operandst

bool is_boolean() const

Return whether the expression represents a Boolean.

bool is_constant() const

Return whether the expression is a constant.

typet & type()

Return the type of the expression.

The Boolean constant false.

void from_integer(const mp_integer &i)

An IEEE 754 floating-point value, including specificiation.

The trinary if-then-else operator.

Unbounded, signed integers (mathematical integers, not bitvectors)

constant_exprt one_expr() const

constant_exprt zero_expr() const

const irep_idt & get(const irep_idt &name) const

const irep_idt & id() const

static void validate(const exprt &, validation_modet)

binding_exprt & binding()

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

Check that the member expression has the right number of operands, refers to a component that exists ...

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

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...

Natural numbers including zero (mathematical integers, not bitvectors)

constant_exprt zero_expr() const

constant_exprt one_expr() const

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

Boolean OR All operands must be boolean, and the result is always boolean.

Unbounded, signed real numbers.

constant_exprt zero_expr() const

constant_exprt one_expr() const

exprt & component(const irep_idt &name, const namespacet &ns)

Structure type, corresponds to C style structs.

The Boolean constant true.

The type of an expression, extends irept.

with_exprt make_with_expr() const

converts an update expr into a (possibly nested) with expression

exprt::operandst & designator()

Operator to update elements in structs and arrays.

Deprecated expression utility functions.

const std::string & id2string(const irep_idt &d)

API to expression classes for Pointers.

Ranges: pair of begin and end iterators, which can be initialized from containers,...

ranget< iteratort > make_range(iteratort begin, iteratort end)

#define CHECK_RETURN(CONDITION)

#define UNREACHABLE

This should be used to mark dead code.

#define DATA_INVARIANT(CONDITION, REASON)

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

#define PRECONDITION(CONDITION)

#define INVARIANT(CONDITION, REASON)

This macro uses the wrapper function 'invariant_violated_string'.

bool operator==(const exprt &lhs, bool rhs)

Return whether the expression lhs is a constant of Boolean type that is representing the Boolean valu...

exprt disjunction(const exprt::operandst &op)

1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...

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

bool operator!=(const exprt &lhs, bool rhs)

Return whether the expression lhs is not a constant of Boolean type or is not representing the Boolea...

exprt conjunction(exprt a, exprt b)

Conjunction of two expressions.

API to expression classes.

const let_exprt & to_let_expr(const exprt &expr)

Cast an exprt to a let_exprt.

const member_exprt & to_member_expr(const exprt &expr)

Cast an exprt to a member_exprt.

const index_designatort & to_index_designator(const exprt &expr)

Cast an exprt to an index_designatort.

const constant_exprt & to_constant_expr(const exprt &expr)

Cast an exprt to a constant_exprt.

const with_exprt & to_with_expr(const exprt &expr)

Cast an exprt to a with_exprt.

const struct_typet & to_struct_type(const typet &type)

Cast a typet to a struct_typet.

const struct_tag_typet & to_struct_tag_type(const typet &type)

Cast a typet to a struct_tag_typet.

const struct_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)

Cast a typet to a struct_or_union_tag_typet.

std::optional< exprt > substitute_symbols(const std::map< irep_idt, exprt > &substitutions, exprt src)

Substitute free occurrences of the variables given by their identifiers in the keys of the map in the...

#define DATA_CHECK(vm, condition, message)

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