26{

28 {

29 if(

35 {

36 return true;

37 }

39 return true;

40 else if(

44 {

45 return true;

46 }

48 return true;

50 return true;

51 }

52

54 return true;

55

56 for(const auto &op : expr.operands())

57 {

59 return true;

60 }

61

62 return false;

63}

66{

68 {

71 return true;

72 }

74 {

76

78 return true;

80 {

82 return true;

83 }

84 }

90 return true;

91

92 return false;

93}

99{

101 return;

102

104 {

107 expr.swap(result);

108 return;

109 }

110

113

115 {

116 if(

122 {

123

124

125

126

131

134

136

137

141

142 for(std::size_t i=0; i<array_expr.operands().size(); i++)

143 {

145

150 }

151

153 }

155 {

159

162

164

165

169

170 for(std::size_t i=0; i<array_expr.operands().size(); i++)

171 {

173

176 }

177

179 }

180 else if(

184 {

185

186

187

191

195

198

199 const bool is_float =

204 {

205 if(is_float)

207 else

209 }

211 {

212 if(is_float)

214 else

216 }

217 else

218 {

219

221 }

222

223 for(std::size_t i = 0; i < dimension; ++i)

224 {

226

227 operands.push_back(

232 zero});

233 }

234

239 }

241 {

243 }

245 {

247

248 if(op.type().id() != ID_array)

249 {

250

260 }

261 else if(

264 {

265

266

272

275

276 for(std::size_t i = 0; i < dimension; i++)

277 {

279 elements.push_back(

281 }

282

286 }

287 }

288 }

289

291}

295{

297 return;

298

300 {

303

304 for(struct_union_typet::componentst::iterator

307 it++)

308 {

310 }

311 }

313 {

315

319 }

323 {

325 }

327 {

329

331

332

336 }

337}

348{

349 for(auto it = symbol_table.begin(); it != symbol_table.end(); ++it)

351}

355{

356 for(auto &i : goto_function.body.instructions)

357 i.transform([](exprt e) -> std::optional<exprt> {

359 {

361 return e;

362 }

363 else

364 return {};

365 });

366}

391{

392 for(auto &function_it : goto_functions.function_map)

393 for(auto &instruction : function_it.second.body.instructions)

394 {

399 });

401 return true;

402 }

403

404 return false;

405}

API to expression classes that are internal to the C frontend.

const shuffle_vector_exprt & to_shuffle_vector_expr(const exprt &expr)

Cast an exprt to a shuffle_vector_exprt.

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

Array constructor from list of elements.

A base class for binary expressions.

A base class for relations, i.e., binary predicates whose two operands have the same type.

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

typet & type()

Return the type of the expression.

const source_locationt & source_location() const

source_locationt & add_source_location()

A collection of goto functions.

function_mapt function_map

::goto_functiont goto_functiont

symbol_tablet symbol_table

Symbol table.

goto_functionst goto_functions

GOTO functions.

The trinary if-then-else operator.

const irep_idt & id() const

Base type for structs and unions.

The symbol table base class interface.

virtual iteratort begin()=0

virtual iteratort end()=0

typet type

Type of symbol.

exprt value

Initial value of symbol.

Semantic type conversion.

static exprt conditional_cast(const exprt &expr, const typet &type)

The type of an expression, extends irept.

const source_locationt & source_location() const

Generic base class for unary expressions.

#define Forall_operands(it, expr)

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

static void remove_vector(typet &)

removes vector data type

static bool have_to_remove_vector(const typet &type)

bool has_vector(const goto_functionst &goto_functions)

returns true iff any of the given goto functions has instructions that use the vector type

Remove the 'vector' data type by compilation into arrays.

#define PRECONDITION(CONDITION)

API to expression classes.

const typecast_exprt & to_typecast_expr(const exprt &expr)

Cast an exprt to a typecast_exprt.

const binary_exprt & to_binary_expr(const exprt &expr)

Cast an exprt to a binary_exprt.

const unary_exprt & to_unary_expr(const exprt &expr)

Cast an exprt to a unary_exprt.

const constant_exprt & to_constant_expr(const exprt &expr)

Cast an exprt to a constant_exprt.

const vector_typet & to_vector_type(const typet &type)

Cast a typet to a vector_typet.

const code_typet & to_code_type(const typet &type)

Cast a typet to a code_typet.

const array_typet & to_array_type(const typet &type)

Cast a typet to an array_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)