CBMC: /home/runner/work/cbmc/cbmc/src/util/expr.h Source File

9#ifndef CPROVER_UTIL_EXPR_H

10#define CPROVER_UTIL_EXPR_H

19#include <functional>

21#define forall_operands(it, expr) \

22 for(exprt::operandst::const_iterator \

23 it = as_const(expr).operands().begin(), \

24 it##_end = as_const(expr).operands().end(); \

25 it != it##_end; \

26 ++it)

28#define Forall_operands(it, expr) \

29 if((expr).has_operands()) \

30 for(exprt::operandst::iterator it=(expr).operands().begin(); \

31 it!=(expr).operands().end(); ++it)

33#define forall_expr(it, expr) \

34 for(exprt::operandst::const_iterator it=(expr).begin(); \

35 it!=(expr).end(); ++it)

37#define Forall_expr(it, expr) \

38 for(exprt::operandst::iterator it=(expr).begin(); \

39 it!=(expr).end(); ++it)

57{

58public:

73 {{ID_type, std::move(_type)}},

75 {

76 }

100

103 {

104 if(location.is_not_nil())

106 return *this;

107 }

108

111 {

112 if(location.is_not_nil())

114 return std::move(*this);

115 }

116

119 {

120 if(other.source_location().is_not_nil())

122 return *this;

123 }

124

127 {

128 if(other.source_location().is_not_nil())

130 return std::move(*this);

131 }

132

133protected:

136

139

142

145

148

151

154

157

158public:

161

168

175

179 {

180 operands().push_back(std::move(expr));

181 }

182

187 {

189 #ifndef USE_LIST

190 op.reserve(op.size() + 2);

191 #endif

192 op.push_back(std::move(e1));

193 op.push_back(std::move(e2));

194 }

195

201 {

203 #ifndef USE_LIST

204 op.reserve(op.size() + 3);

205 #endif

206 op.push_back(std::move(e1));

207 op.push_back(std::move(e2));

208 op.push_back(std::move(e3));

209 }

210

217

218 DEPRECATED(SINCE(2025, 7, 5, "use expr == true instead"))

226

233

235

240

245

250

259 static void

263

273 const exprt &expr,

276 {

278 }

279

289 const exprt &expr,

292 {

293

295 {

297 }

298

299

301

303

305 }

306

307protected:

309 {

310 return static_cast<exprt &>(add(name));

311 }

312

314 {

315 return static_cast<const exprt &>(find(name));

316 }

317

318public:

325 void visit_pre(std::function<void(const exprt &)>) const;

326

331 void visit_post(std::function<void(const exprt &)>) const;

332

344};

345

350{

351protected:

352

357

362

363

370};

371

378

385

386#endif

void validate_expr(const shuffle_vector_exprt &value)

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

virtual void operator()(const exprt &)

virtual ~const_expr_visitort()

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

Base class for all expressions.

expr_protectedt(irep_idt _id, typet _type)

expr_protectedt(irep_idt _id, typet _type, operandst _operands)

virtual void operator()(exprt &)

Base class for all expressions.

const source_locationt & find_source_location() const

Get a source_locationt from the expression or from its operands (non-recursively).

std::vector< exprt > operandst

const typet & type() const

bool is_one() const

Return whether the expression is a constant representing 1.

bool has_operands() const

Return true if there is at least one operand.

void add_to_operands(exprt &&e1, exprt &&e2, exprt &&e3)

Add the given arguments to the end of exprt's operands.

bool is_true() const

Return whether the expression is a constant representing true.

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

Check that the expression is well-formed, assuming that its subexpressions and type have all ready be...

void copy_to_operands(const exprt &expr)

Copy the given argument to the end of exprt's operands.

depth_iteratort depth_end()

const_depth_iteratort depth_cend() const

exprt && with_source_location(source_locationt location) &&

Add the source location from location, if it is non-nil.

const_unique_depth_iteratort unique_depth_end() const

bool is_boolean() const

Return whether the expression represents a Boolean.

depth_iteratort depth_begin()

const_unique_depth_iteratort unique_depth_cend() const

void visit(class expr_visitort &visitor)

These are pre-order traversal visitors, i.e., the visitor is executed on a node before its children h...

bool is_false() const

Return whether the expression is a constant representing false.

void reserve_operands(operandst::size_type n)

bool is_zero() const

Return whether the expression is a constant representing 0.

void visit_pre(std::function< void(exprt &)>)

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

Check that the expression is well-formed (full check, including checks of all subexpressions and the ...

exprt(irep_idt _id, typet _type)

exprt & add_expr(const irep_idt &name)

const exprt & op0() const

exprt(irep_idt _id, typet _type, operandst &&_operands)

bool is_constant() const

Return whether the expression is a constant.

exprt && with_source_location(const exprt &other) &&

Add the source location from other, if it has any.

typet & type()

Return the type of the expression.

exprt(const irep_idt &_id)

const_depth_iteratort depth_cbegin() const

const exprt & find_expr(const irep_idt &name) const

void visit_post(std::function< void(exprt &)>)

These are post-order traversal visitors, i.e., the visitor is executed on a node after its children h...

exprt & with_source_location(const exprt &other) &

Add the source location from other, if it has any.

const operandst & operands() const

void add_to_operands(exprt &&e1, exprt &&e2)

Add the given arguments to the end of exprt's operands.

void add_to_operands(exprt &&expr)

Add the given argument to the end of exprt's operands.

exprt(const irep_idt &id, typet type, source_locationt loc)

const source_locationt & source_location() const

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

Check that the expression is well-formed (shallow checks only, i.e., subexpressions and its type are ...

source_locationt & add_source_location()

void drop_source_location()

const exprt & op3() const

const_unique_depth_iteratort unique_depth_cbegin() const

const exprt & op2() const

void add_to_operands(const exprt &expr)

Add the given argument to the end of exprt's operands.

const_unique_depth_iteratort unique_depth_begin() const

const exprt & op1() const

exprt & with_source_location(source_locationt location) &

Add the source location from location, if it is non-nil.

There are a large number of kinds of tree structured or tree-like data in CPROVER.

const irept & find(const irep_idt &name) const

void remove(const irep_idt &name)

const irep_idt & id() const

irept & add(const irep_idt &name)

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

The type of an expression, extends irept.

#define SINCE(year, month, day, msg)

Defines typet, type_with_subtypet and type_with_subtypest.

void check_expr(const exprt &expr, const validation_modet vm)

Check that the given expression is well-formed (shallow checks only, i.e., subexpressions and its typ...

void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)

Check that the given expression is well-formed (full check, including checks of all subexpressions an...

void validate_full_type(const typet &type, const namespacet &ns, const validation_modet vm)

Check that the given type is well-formed (full check, including checks of subtypes)