CBMC: /home/runner/work/cbmc/cbmc/src/analyses/ai.cpp Source File

20 void ai_baset::output(

21 const namespacet &ns,

22 const goto_functionst &goto_functions,

23 std::ostream &out) const

24{

25 for(const auto &gf_entry : goto_functions.function_map)

26 {

27 if(gf_entry.second.body_available())

28 {

29 out << "////\n";

30 out << "//// Function: " << gf_entry.first << "\n";

31 out << "////\n";

32 out << "\n";

33

34 output(ns, gf_entry.first, gf_entry.second.body, out);

35 }

36 }

37}

39 void ai_baset::output(

40 const namespacet &ns,

41 const irep_idt &function_id,

42 const goto_programt &goto_program,

43 std::ostream &out) const

44{

45 (void)function_id; // unused parameter

46

47 forall_goto_program_instructions(i_it, goto_program)

48 {

49 out << "**** " << i_it->location_number << " " << i_it->source_location()

50 << "\n";

51

52 abstract_state_before(i_it)->output(out, *this, ns);

53 out << "\n";

54 #if 1

55 i_it->output(out);

56 out << "\n";

57 #endif

58 }

59}

61 jsont ai_baset::output_json(

62 const namespacet &ns,

63 const goto_functionst &goto_functions) const

64{

65 json_objectt result;

66

67 for(const auto &gf_entry : goto_functions.function_map)

68 {

69 if(gf_entry.second.body_available())

70 {

71 result[id2string(gf_entry.first)] =

72 output_json(ns, gf_entry.first, gf_entry.second.body);

73 }

74 else

75 {

76 result[id2string(gf_entry.first)] = json_arrayt();

77 }

78 }

79

80 return std::move(result);

81}

83 jsont ai_baset::output_json(

84 const namespacet &ns,

85 const irep_idt &function_id,

86 const goto_programt &goto_program) const

87{

88 (void)function_id; // unused parameter

89

90 json_arrayt contents;

91

92 forall_goto_program_instructions(i_it, goto_program)

93 {

94 // Ideally we need output_instruction_json

95 std::ostringstream out;

96 i_it->output(out);

97

98 json_objectt location{

99 {"locationNumber", json_numbert(std::to_string(i_it->location_number))},

100 {"sourceLocation", json_stringt(i_it->source_location().as_string())},

101 {"abstractState", abstract_state_before(i_it)->output_json(*this, ns)},

102 {"instruction", json_stringt(out.str())}};

103

104 contents.push_back(std::move(location));

105 }

106

107 return std::move(contents);

108}

110 xmlt ai_baset::output_xml(

111 const namespacet &ns,

112 const goto_functionst &goto_functions) const

113{

114 xmlt program("program");

115

116 for(const auto &gf_entry : goto_functions.function_map)

117 {

118 xmlt function(

119 "function",

120 {{"name", id2string(gf_entry.first)},

121 {"body_available", gf_entry.second.body_available() ? "true" : "false"}},

122 {});

123

124 if(gf_entry.second.body_available())

125 {

126 function.new_element(

127 output_xml(ns, gf_entry.first, gf_entry.second.body));

128 }

129

130 program.new_element(function);

131 }

132

133 return program;

134}

136 xmlt ai_baset::output_xml(

137 const namespacet &ns,

138 const irep_idt &function_id,

139 const goto_programt &goto_program) const

140{

141 (void)function_id; // unused parameter

142

143 xmlt function_body;

144

145 forall_goto_program_instructions(i_it, goto_program)

146 {

147 xmlt location(

148 "",

149 {{"location_number", std::to_string(i_it->location_number)},

150 {"source_location", i_it->source_location().as_string()}},

151 {abstract_state_before(i_it)->output_xml(*this, ns)});

152

153 // Ideally we need output_instruction_xml

154 std::ostringstream out;

155 i_it->output(out);

156 location.set_attribute("instruction", out.str());

157

158 function_body.new_element(location);

159 }

160

161 return function_body;

162}

165 ai_baset::entry_state(const goto_functionst &goto_functions)

166{

167 // find the 'entry function'

168

169 goto_functionst::function_mapt::const_iterator

170 f_it=goto_functions.function_map.find(goto_functions.entry_point());

171

172 if(f_it!=goto_functions.function_map.end())

173 return entry_state(f_it->second.body);

174

175 // It is not clear if this is even a well-structured goto_functionst object

176 return nullptr;

177}

179 ai_baset::trace_ptrt ai_baset::entry_state(const goto_programt &goto_program)

180{

181 if(goto_program.empty())

182 return nullptr;

183

184 // The first instruction of 'goto_program' is the entry point

185 trace_ptrt p = history_factory->epoch(goto_program.instructions.begin());

186 get_state(p).make_entry();

187 return p;

188}

190 void ai_baset::initialize(

191 const irep_idt &function_id,

192 const goto_functionst::goto_functiont &goto_function)

193{

194 initialize(function_id, goto_function.body);

195}

197 void ai_baset::initialize(const irep_idt &, const goto_programt &goto_program)

198{

199 // Domains are created and set to bottom on access.

200 // So we do not need to set them to be bottom before hand.

201}

203 void ai_baset::initialize(const goto_functionst &goto_functions)

204{

205 for(const auto &gf_entry : goto_functions.function_map)

206 initialize(gf_entry.first, gf_entry.second);

207}

209 void ai_baset::finalize()

210{

211 // Nothing to do per default

212}

214 ai_baset::trace_ptrt ai_baset::get_next(working_sett &working_set)

215{

216 PRECONDITION(!working_set.empty());

217

218 static_assert(

219 std::is_same<

220 working_sett,

221 std::set<trace_ptrt, ai_history_baset::compare_historyt>>::value,

222 "begin must return the minimal entry");

223 auto first = working_set.begin();

224

225 trace_ptrt t = *first;

226

227 working_set.erase(first);

228

229 return t;

230}

232 bool ai_baset::fixedpoint(

233 trace_ptrt start_trace,

234 const irep_idt &function_id,

235 const goto_programt &goto_program,

236 const goto_functionst &goto_functions,

237 const namespacet &ns)

238{

239 PRECONDITION(start_trace != nullptr);

240

241 working_sett working_set;

242 put_in_working_set(working_set, start_trace);

243

244 bool new_data=false;

245

246 while(!working_set.empty())

247 {

248 trace_ptrt p = get_next(working_set);

249

250 // goto_program is really only needed for iterator manipulation

251 if(visit(function_id, p, working_set, goto_program, goto_functions, ns))

252 new_data=true;

253 }

254

255 return new_data;

256}

258 void ai_baset::fixedpoint(

259 trace_ptrt start_trace,

260 const goto_functionst &goto_functions,

261 const namespacet &ns)

262{

263 goto_functionst::function_mapt::const_iterator f_it =

264 goto_functions.function_map.find(goto_functions.entry_point());

265

266 if(f_it != goto_functions.function_map.end())

267 fixedpoint(start_trace, f_it->first, f_it->second.body, goto_functions, ns);

268}

270 bool ai_baset::visit(

271 const irep_idt &function_id,

272 trace_ptrt p,

273 working_sett &working_set,

274 const goto_programt &goto_program,

275 const goto_functionst &goto_functions,

276 const namespacet &ns)

277{

278 bool new_data=false;

279 locationt l = p->current_location();

280 messaget log(message_handler);

281

282 log.progress() << "ai_baset::visit " << l->location_number << " in "

283 << function_id << messaget::eom;

284

285 // Function call and end are special cases

286 if(l->is_function_call())

287 {

288 DATA_INVARIANT(

289 goto_program.get_successors(l).size() == 1,

290 "function calls only have one successor");

291

292 DATA_INVARIANT(

293 *(goto_program.get_successors(l).begin()) == std::next(l),

294 "function call successor / return location must be the next instruction");

295

296 new_data = visit_function_call(

297 function_id, p, working_set, goto_program, goto_functions, ns);

298 }

299 else if(l->is_end_function())

300 {

301 DATA_INVARIANT(

302 goto_program.get_successors(l).empty(),

303 "The end function instruction should have no successors.");

304

305 new_data = visit_end_function(

306 function_id, p, working_set, goto_program, goto_functions, ns);

307 }

308 else

309 {

310 // Successors can be empty, for example assume(0).

311 // Successors can contain duplicates, for example GOTO next;

312 for(const auto &to_l : goto_program.get_successors(l))

313 {

314 if(to_l == goto_program.instructions.end())

315 continue;

316

317 new_data |= visit_edge(

318 function_id,

319 p,

320 function_id,

321 to_l,

322 ai_history_baset::no_caller_history,

323 ns,

324 working_set); // Local steps so no caller history needed

325 }

326 }

327

328 return new_data;

329}

331 bool ai_baset::visit_edge(

332 const irep_idt &function_id,

333 trace_ptrt p,

334 const irep_idt &to_function_id,

335 locationt to_l,

336 trace_ptrt caller_history,

337 const namespacet &ns,

338 working_sett &working_set)

339{

340 messaget log(message_handler);

341 log.progress() << "ai_baset::visit_edge from "

342 << p->current_location()->location_number << " to "

343 << to_l->location_number << "... ";

344

345 // Has history taught us not to step here...

346 auto next =

347 p->step(to_l, *(storage->abstract_traces_before(to_l)), caller_history);

348 if(next.first == ai_history_baset::step_statust::BLOCKED)

349 {

350 log.progress() << "blocked by history" << messaget::eom;

351 return false;

352 }

353 else if(next.first == ai_history_baset::step_statust::NEW)

354 {

355 log.progress() << "gives a new history... ";

356 }

357 else

358 {

359 log.progress() << "merges with existing history... ";

360 }

361 trace_ptrt to_p = next.second;

362

363 // Abstract domains are mutable so we must copy before we transform

364 statet &current = get_state(p);

365

366 std::unique_ptr<statet> tmp_state(make_temporary_state(current));

367 statet &new_values = *tmp_state;

368

369 // Apply transformer

370 log.progress() << "applying transformer... ";

371 new_values.transform(function_id, p, to_function_id, to_p, *this, ns);

372

373 // Expanding a domain means that it has to be analysed again

374 // Likewise if the history insists that it is a new trace

375 // (assuming it is actually reachable).

376 log.progress() << "merging... ";

377 bool return_value = false;

378 if(

379 merge(new_values, p, to_p) ||

380 (next.first == ai_history_baset::step_statust::NEW &&

381 !new_values.is_bottom()))

382 {

383 put_in_working_set(working_set, to_p);

384 log.progress() << "result queued." << messaget::eom;

385 return_value = true;

386 }

387 else

388 {

389 log.progress() << "domain unchanged." << messaget::eom;

390 }

391

392 // Branch because printing some histories and domains can be expensive

393 // esp. if the output is then just discarded and this is a critical path.

394 if(message_handler.get_verbosity() >= messaget::message_levelt::M_DEBUG)

395 {

396 log.debug() << "p = ";

397 p->output(log.debug());

398 log.debug() << messaget::eom;

399

400 log.debug() << "current = ";

401 current.output(log.debug(), *this, ns);

402 log.debug() << messaget::eom;

403

404 log.debug() << "to_p = ";

405 to_p->output(log.debug());

406 log.debug() << messaget::eom;

407

408 log.debug() << "new_values = ";

409 new_values.output(log.debug(), *this, ns);

410 log.debug() << messaget::eom;

411 }

412

413 return return_value;

414}

416 bool ai_baset::visit_edge_function_call(

417 const irep_idt &calling_function_id,

418 trace_ptrt p_call,

419 locationt l_return,

420 const irep_idt &,

421 working_sett &working_set,

422 const goto_programt &,

423 const goto_functionst &,

424 const namespacet &ns)

425{

426 messaget log(message_handler);

427 log.progress() << "ai_baset::visit_edge_function_call from "

428 << p_call->current_location()->location_number << " to "

429 << l_return->location_number << messaget::eom;

430

431 // The default implementation is not interprocedural

432 // so the effects of the call are approximated but nothing else

433 return visit_edge(

434 calling_function_id,

435 p_call,

436 calling_function_id,

437 l_return,

438 ai_history_baset::

439 no_caller_history, // Not needed as we are skipping the function call

440 ns,

441 working_set);

442}

444 bool ai_baset::visit_function_call(

445 const irep_idt &calling_function_id,

446 trace_ptrt p_call,

447 working_sett &working_set,

448 const goto_programt &caller,

449 const goto_functionst &goto_functions,

450 const namespacet &ns)

451{

452 locationt l_call = p_call->current_location();

453

454 PRECONDITION(l_call->is_function_call());

455

456 messaget log(message_handler);

457 log.progress() << "ai_baset::visit_function_call at "

458 << l_call->location_number << messaget::eom;

459

460 locationt l_return = std::next(l_call);

461

462 // operator() allows analysis of a single goto_program independently

463 // it generates a synthetic goto_functions object for this

464 if(!goto_functions.function_map.empty())

465 {

466 const exprt &callee_expression = l_call->call_function();

467

468 if(callee_expression.id() == ID_symbol)

469 {

470 const irep_idt &callee_function_id =

471 to_symbol_expr(callee_expression).identifier();

472

473 log.progress() << "Calling " << callee_function_id << messaget::eom;

474

475 goto_functionst::function_mapt::const_iterator it =

476 goto_functions.function_map.find(callee_function_id);

477

478 DATA_INVARIANT(

479 it != goto_functions.function_map.end(),

480 "Function " + id2string(callee_function_id) + "not in function map");

481

482 const goto_functionst::goto_functiont &callee_fun = it->second;

483

484 if(callee_fun.body_available())

485 {

486 return visit_edge_function_call(

487 calling_function_id,

488 p_call,

489 l_return,

490 callee_function_id,

491 working_set,

492 callee_fun.body,

493 goto_functions,

494 ns);

495 }

496 else

497 {

498 // Fall through to the default, body not available, case

499 }

500 }

501 else

502 {

503 // Function pointers are not currently supported and must be removed

504 DATA_INVARIANT(

505 callee_expression.id() == ID_symbol,

506 "Function pointers and indirect calls must be removed before "

507 "analysis.");

508 }

509 }

510

511 // If the body is not available then we just do the edge from call to return

512 // in the caller. Domains should over-approximate what the function might do.

513 return visit_edge(

514 calling_function_id,

515 p_call,

516 calling_function_id,

517 l_return,

518 ai_history_baset::no_caller_history, // Would be the same as p_call...

519 ns,

520 working_set);

521}

523 bool ai_baset::visit_end_function(

524 const irep_idt &function_id,

525 trace_ptrt p,

526 working_sett &working_set,

527 const goto_programt &goto_program,

528 const goto_functionst &goto_functions,

529 const namespacet &ns)

530{

531 locationt l = p->current_location();

532 PRECONDITION(l->is_end_function());

533

534 messaget log(message_handler);

535 log.progress() << "ai_baset::visit_end_function " << function_id

536 << messaget::eom;

537

538 // Do nothing

539 return false;

540}

542 bool ai_recursive_interproceduralt::visit_edge_function_call(

543 const irep_idt &calling_function_id,

544 trace_ptrt p_call,

545 locationt l_return,

546 const irep_idt &callee_function_id,

547 working_sett &working_set,

548 const goto_programt &callee,

549 const goto_functionst &goto_functions,

550 const namespacet &ns)

551{

552 messaget log(message_handler);

553 log.progress() << "ai_recursive_interproceduralt::visit_edge_function_call"

554 << " from " << p_call->current_location()->location_number

555 << " to " << l_return->location_number << messaget::eom;

556

557 // This is the edge from call site to function head.

558 {

559 locationt l_begin = callee.instructions.begin();

560

561 working_sett catch_working_set; // The trace from the next fixpoint

562

563 // Do the edge from the call site to the beginning of the function

564 bool new_data = visit_edge(

565 calling_function_id,

566 p_call,

567 callee_function_id,

568 l_begin,

569 ai_history_baset::

570 no_caller_history, // Not needed as p_call already has the info

571 ns,

572 catch_working_set);

573

574 log.progress() << "Handle " << callee_function_id << " recursively"

575 << messaget::eom;

576

577 // do we need to do/re-do the fixedpoint of the body?

578 if(new_data)

579 fixedpoint(

580 get_next(catch_working_set),

581 callee_function_id,

582 callee,

583 goto_functions,

584 ns);

585 }

586

587 // This is the edge from function end to return site.

588 {

589 log.progress() << "Handle return edges" << messaget::eom;

590

591 // get location at end of the procedure we have called

592 locationt l_end = --callee.instructions.end();

593 DATA_INVARIANT(

594 l_end->is_end_function(),

595 "The last instruction of a goto_program must be END_FUNCTION");

596

597 // Find the histories for a location

598 auto traces = storage->abstract_traces_before(l_end);

599

600 bool new_data = false;

601

602 // The history used may mean there are multiple histories at the end of the

603 // function. Some of these can be progressed (for example, if the history

604 // tracks paths within functions), some can't be (for example, not all

605 // calling contexts will be appropriate). We rely on the history's step,

606 // called from visit_edge to prune as applicable.

607 for(auto p_end : *traces)

608 {

609 // do edge from end of function to instruction after call

610 const statet &end_state = get_state(p_end);

611

612 if(!end_state.is_bottom())

613 {

614 // function exit point reachable in that history

615

616 new_data |= visit_edge(

617 callee_function_id,

618 p_end,

619 calling_function_id,

620 l_return,

621 p_call, // To allow function-local history

622 ns,

623 working_set);

624 }

625 }

626

627 return new_data;

628 }

629}

ai.h

Abstract Interpretation.

ai_baset::locationt

goto_programt::const_targett locationt

Definition ai.h:124

ai_baset::visit

virtual bool visit(const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)

Perform one step of abstract interpretation from trace t Depending on the instruction type it may com...

Definition ai.cpp:270

ai_baset::storage

std::unique_ptr< ai_storage_baset > storage

Definition ai.h:515

ai_baset::get_state

virtual statet & get_state(trace_ptrt p)

Get the state for the given history, creating it with the factory if it doesn't exist.

Definition ai.h:519

ai_baset::visit_edge

bool visit_edge(const irep_idt &function_id, trace_ptrt p, const irep_idt &to_function_id, locationt to_l, trace_ptrt caller_history, const namespacet &ns, working_sett &working_set)

Definition ai.cpp:331

ai_baset::output

virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const

Output the abstract states for a single function.

Definition ai.cpp:39

ai_baset::message_handler

message_handlert & message_handler

Definition ai.h:525

ai_baset::visit_end_function

virtual bool visit_end_function(const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)

Definition ai.cpp:523

ai_baset::visit_function_call

virtual bool visit_function_call(const irep_idt &function_id, trace_ptrt p_call, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)

Definition ai.cpp:444

ai_baset::entry_state

trace_ptrt entry_state(const goto_programt &goto_program)

Set the abstract state of the entry location of a single function to the entry state required by the ...

Definition ai.cpp:179

ai_baset::visit_edge_function_call

virtual bool visit_edge_function_call(const irep_idt &calling_function_id, trace_ptrt p_call, locationt l_return, const irep_idt &callee_function_id, working_sett &working_set, const goto_programt &callee, const goto_functionst &goto_functions, const namespacet &ns)

Definition ai.cpp:416

ai_baset::initialize

virtual void initialize(const irep_idt &function_id, const goto_programt &goto_program)

Initialize all the abstract states for a single function.

Definition ai.cpp:197

ai_baset::fixedpoint

virtual bool fixedpoint(trace_ptrt starting_trace, const irep_idt &function_id, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)

Run the fixedpoint algorithm until it reaches a fixed point.

Definition ai.cpp:232

ai_baset::make_temporary_state

virtual std::unique_ptr< statet > make_temporary_state(const statet &s)

Make a copy of a state.

Definition ai.h:509

ai_baset::trace_ptrt

ai_history_baset::trace_ptrt trace_ptrt

Definition ai.h:121

ai_baset::put_in_working_set

void put_in_working_set(working_sett &working_set, trace_ptrt t)

Definition ai.h:423

ai_baset::get_next

trace_ptrt get_next(working_sett &working_set)

Get the next location from the work queue.

Definition ai.cpp:214

ai_baset::working_sett

trace_sett working_sett

The work queue, sorted using the history's ordering operator.

Definition ai.h:418

ai_baset::merge

virtual bool merge(const statet &src, trace_ptrt from, trace_ptrt to)

Merge the state src, flowing from tracet from to tracet to, into the state currently stored for trace...

Definition ai.h:502

ai_baset::abstract_state_before

virtual cstate_ptrt abstract_state_before(locationt l) const

Get a copy of the abstract state before the given instruction, without needing to know what kind of d...

Definition ai.h:225

ai_baset::output_xml

virtual xmlt output_xml(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const

Output the abstract states for a single function as XML.

Definition ai.cpp:136

ai_baset::output_json

virtual jsont output_json(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const

Output the abstract states for a single function as JSON.

Definition ai.cpp:83

ai_baset::history_factory

std::unique_ptr< ai_history_factory_baset > history_factory

For creating history objects.

Definition ai.h:495

ai_baset::finalize

virtual void finalize()

Override this to add a cleanup or post-processing step after fixedpoint has run.

Definition ai.cpp:209

ai_domain_baset

The interface offered by a domain, allows code to manipulate domains without knowing their exact type...

Definition ai_domain.h:54

ai_domain_baset::output

virtual void output(std::ostream &, const ai_baset &, const namespacet &) const

Definition ai_domain.h:104

ai_history_baset

A history object is an abstraction / representation of the control-flow part of a set of traces.

Definition ai_history.h:37

ai_history_baset::step_statust::NEW

@ NEW

ai_history_baset::step_statust::BLOCKED

@ BLOCKED

ai_history_baset::no_caller_history

static const trace_ptrt no_caller_history

Definition ai_history.h:121

ai_recursive_interproceduralt::visit_edge_function_call

bool visit_edge_function_call(const irep_idt &calling_function_id, trace_ptrt p_call, locationt l_return, const irep_idt &callee_function_id, working_sett &working_set, const goto_programt &callee, const goto_functionst &goto_functions, const namespacet &ns) override

Definition ai.cpp:542

ait

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

Definition ai.h:566

dstringt

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

Definition dstring.h:38

exprt

Base class for all expressions.

Definition expr.h:57

goto_functionst

A collection of goto functions.

Definition goto_functions.h:25

goto_functionst::function_map

function_mapt function_map

Definition goto_functions.h:29

goto_functionst::goto_functiont

::goto_functiont goto_functiont

Definition goto_functions.h:27

goto_functionst::entry_point

static irep_idt entry_point()

Get the identifier of the entry point to a goto model.

Definition goto_functions.h:97

goto_programt

A generic container class for the GOTO intermediate representation of one function.

Definition goto_program.h:72

goto_programt::instructions

instructionst instructions

The list of instructions in the goto program.

Definition goto_program.h:621

goto_programt::get_successors

std::list< Target > get_successors(Target target) const

Get control-flow successors of a given instruction.

Definition goto_program.h:1125

goto_programt::empty

bool empty() const

Is the program empty?

Definition goto_program.h:798

json_arrayt

Definition json.h:165

json_numbert

Definition json.h:289

json_objectt

Definition json.h:298

json_stringt

Definition json.h:270

jsont

Definition json.h:27

message_handlert::get_verbosity

unsigned get_verbosity() const

Definition message.h:53

messaget

Class that provides messages with a built-in verbosity 'level'.

Definition message.h:154

messaget::M_DEBUG

@ M_DEBUG

Definition message.h:170

messaget::eom

static eomt eom

Definition message.h:289

namespacet

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

Definition namespace.h:91

xmlt

Definition xml.h:21

xmlt::new_element

xmlt & new_element(const std::string &key)

Definition xml.h:95

forall_goto_program_instructions

#define forall_goto_program_instructions(it, program)

Definition goto_program.h:1228

id2string

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

Definition irep.h:44

log

double log(double x)

Definition math.c:2416

invariant.h

DATA_INVARIANT

#define DATA_INVARIANT(CONDITION, REASON)

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

Definition invariant.h:534

PRECONDITION

#define PRECONDITION(CONDITION)

Definition invariant.h:463

to_symbol_expr

const symbol_exprt & to_symbol_expr(const exprt &expr)

Cast an exprt to a symbol_exprt.

Definition std_expr.h:221