cprover
Loading...
Searching...
No Matches
ai.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Abstract Interpretation
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
44
45#ifndef CPROVER_ANALYSES_AI_H
46#define CPROVER_ANALYSES_AI_H
47
48#include <iosfwd>
49#include <memory>
50
51#include <util/deprecate.h>
52#include <util/json.h>
53#include <util/make_unique.h>
54#include <util/message.h>
55#include <util/xml.h>
56
58
59#include "ai_domain.h"
60#include "ai_history.h"
61#include "ai_storage.h"
62#include "is_threaded.h"
63
116
118{
119public:
126
128 std::unique_ptr<ai_history_factory_baset> &&hf,
129 std::unique_ptr<ai_domain_factory_baset> &&df,
130 std::unique_ptr<ai_storage_baset> &&st,
132 : history_factory(std::move(hf)),
133 domain_factory(std::move(df)),
134 storage(std::move(st)),
136 {
137 }
138
139 virtual ~ai_baset()
140 {
141 }
142
145 const irep_idt &function_id,
146 const goto_programt &goto_program,
147 const namespacet &ns)
148 {
149 goto_functionst goto_functions;
150 initialize(function_id, goto_program);
151 trace_ptrt p = entry_state(goto_program);
152 fixedpoint(p, function_id, goto_program, goto_functions, ns);
153 finalize();
154 }
155
158 const goto_functionst &goto_functions,
159 const namespacet &ns)
160 {
161 initialize(goto_functions);
162 trace_ptrt p = entry_state(goto_functions);
163 fixedpoint(p, goto_functions, ns);
164 finalize();
165 }
166
168 void operator()(const abstract_goto_modelt &goto_model)
169 {
170 const namespacet ns(goto_model.get_symbol_table());
171 initialize(goto_model.get_goto_functions());
172 trace_ptrt p = entry_state(goto_model.get_goto_functions());
173 fixedpoint(p, goto_model.get_goto_functions(), ns);
174 finalize();
175 }
176
179 const irep_idt &function_id,
180 const goto_functionst::goto_functiont &goto_function,
181 const namespacet &ns)
182 {
183 goto_functionst goto_functions;
184 initialize(function_id, goto_function);
185 trace_ptrt p = entry_state(goto_function.body);
186 fixedpoint(p, function_id, goto_function.body, goto_functions, ns);
187 finalize();
188 }
189
199
206 {
209 INVARIANT(!l->is_end_function(), "No state after the last instruction");
210 return storage->abstract_traces_before(std::next(l));
211 }
212
226
236 {
239 INVARIANT(!l->is_end_function(), "No state after the last instruction");
240 return abstract_state_before(std::next(l));
241 }
242
245 {
247 }
248
250 {
251 locationt l = p->current_location();
252 INVARIANT(!l->is_end_function(), "No state after the last instruction");
253
254 locationt n = std::next(l);
255
256 auto step_return = p->step(
257 n,
260 // Caller history not needed as this is a local step
261
262 return storage->abstract_state_before(step_return.second, *domain_factory);
263 }
264
266 virtual void clear()
267 {
268 storage->clear();
269 }
270
277 virtual void output(
278 const namespacet &ns,
279 const irep_idt &function_id,
280 const goto_programt &goto_program,
281 std::ostream &out) const;
282
289 virtual jsont output_json(
290 const namespacet &ns,
291 const irep_idt &function_id,
292 const goto_programt &goto_program) const;
293
300 virtual xmlt output_xml(
301 const namespacet &ns,
302 const irep_idt &function_id,
303 const goto_programt &goto_program) const;
304
306 virtual void output(
307 const namespacet &ns,
308 const goto_functionst &goto_functions,
309 std::ostream &out) const;
310
312 void output(
313 const goto_modelt &goto_model,
314 std::ostream &out) const
315 {
316 const namespacet ns(goto_model.symbol_table);
317 output(ns, goto_model.goto_functions, out);
318 }
319
321 void output(
322 const namespacet &ns,
323 const goto_functionst::goto_functiont &goto_function,
324 std::ostream &out) const
325 {
326 output(ns, irep_idt(), goto_function.body, out);
327 }
328
330 virtual jsont output_json(
331 const namespacet &ns,
332 const goto_functionst &goto_functions) const;
333
336 const goto_modelt &goto_model) const
337 {
338 const namespacet ns(goto_model.symbol_table);
339 return output_json(ns, goto_model.goto_functions);
340 }
341
344 const namespacet &ns,
345 const goto_programt &goto_program) const
346 {
347 return output_json(ns, irep_idt(), goto_program);
348 }
349
352 const namespacet &ns,
353 const goto_functionst::goto_functiont &goto_function) const
354 {
355 return output_json(ns, irep_idt(), goto_function.body);
356 }
357
359 virtual xmlt output_xml(
360 const namespacet &ns,
361 const goto_functionst &goto_functions) const;
362
365 const goto_modelt &goto_model) const
366 {
367 const namespacet ns(goto_model.symbol_table);
368 return output_xml(ns, goto_model.goto_functions);
369 }
370
373 const namespacet &ns,
374 const goto_programt &goto_program) const
375 {
376 return output_xml(ns, irep_idt(), goto_program);
377 }
378
381 const namespacet &ns,
382 const goto_functionst::goto_functiont &goto_function) const
383 {
384 return output_xml(ns, irep_idt(), goto_function.body);
385 }
386
387protected:
390 virtual void
391 initialize(const irep_idt &function_id, const goto_programt &goto_program);
392
394 virtual void initialize(
395 const irep_idt &function_id,
396 const goto_functionst::goto_functiont &goto_function);
397
400 virtual void initialize(const goto_functionst &goto_functions);
401
404 virtual void finalize();
405
408 trace_ptrt entry_state(const goto_programt &goto_program);
409
412 trace_ptrt entry_state(const goto_functionst &goto_functions);
413
416
418 trace_ptrt get_next(working_sett &working_set);
419
421 {
422 working_set.insert(t);
423 }
424
427 virtual bool fixedpoint(
428 trace_ptrt starting_trace,
429 const irep_idt &function_id,
430 const goto_programt &goto_program,
431 const goto_functionst &goto_functions,
432 const namespacet &ns);
433
434 virtual void fixedpoint(
435 trace_ptrt starting_trace,
436 const goto_functionst &goto_functions,
437 const namespacet &ns);
438
443 virtual bool visit(
444 const irep_idt &function_id,
445 trace_ptrt p,
446 working_sett &working_set,
447 const goto_programt &goto_program,
448 const goto_functionst &goto_functions,
449 const namespacet &ns);
450
451 // function calls and return are special cases
452 // different kinds of analysis handle these differently so these are virtual
453 // visit_function_call handles which function(s) to call,
454 // while visit_edge_function_call handles a single call
455 virtual bool visit_function_call(
456 const irep_idt &function_id,
457 trace_ptrt p_call,
458 working_sett &working_set,
459 const goto_programt &goto_program,
460 const goto_functionst &goto_functions,
461 const namespacet &ns);
462
463 virtual bool visit_end_function(
464 const irep_idt &function_id,
465 trace_ptrt p,
466 working_sett &working_set,
467 const goto_programt &goto_program,
468 const goto_functionst &goto_functions,
469 const namespacet &ns);
470
471 // The most basic step, computing one edge / transformer application.
472 bool visit_edge(
473 const irep_idt &function_id,
474 trace_ptrt p,
475 const irep_idt &to_function_id,
476 locationt to_l,
477 trace_ptrt caller_history,
478 const namespacet &ns,
479 working_sett &working_set);
480
481 virtual bool visit_edge_function_call(
482 const irep_idt &calling_function_id,
483 trace_ptrt p_call,
484 locationt l_return,
485 const irep_idt &callee_function_id,
486 working_sett &working_set,
487 const goto_programt &callee,
488 const goto_functionst &goto_functions,
489 const namespacet &ns);
490
492 std::unique_ptr<ai_history_factory_baset> history_factory;
493
495 std::unique_ptr<ai_domain_factory_baset> domain_factory;
496
499 virtual bool merge(const statet &src, trace_ptrt from, trace_ptrt to)
500 {
501 statet &dest = get_state(to);
502 return domain_factory->merge(dest, src, from, to);
503 }
504
506 virtual std::unique_ptr<statet> make_temporary_state(const statet &s)
507 {
508 return domain_factory->copy(s);
509 }
510
511 // Domain and history storage
512 std::unique_ptr<ai_storage_baset> storage;
513
517 {
518 return storage->get_state(p, *domain_factory);
519 }
520
521 // Logging
523};
524
525// Perform interprocedural analysis by simply recursing in the interpreter
526// This can lead to a call stack overflow if the domain has a large height
528{
529public:
531 std::unique_ptr<ai_history_factory_baset> &&hf,
532 std::unique_ptr<ai_domain_factory_baset> &&df,
533 std::unique_ptr<ai_storage_baset> &&st,
535 : ai_baset(std::move(hf), std::move(df), std::move(st), mh)
536 {
537 }
538
539protected:
540 // Override the function that handles a single function call edge
542 const irep_idt &calling_function_id,
543 trace_ptrt p_call,
544 locationt l_return,
545 const irep_idt &callee_function_id,
546 working_sett &working_set,
547 const goto_programt &callee,
548 const goto_functionst &goto_functions,
549 const namespacet &ns) override;
550};
551
561template <typename domainT>
563{
564public:
565 // constructor
575
576 explicit ait(std::unique_ptr<ai_domain_factory_baset> &&df)
580 std::move(df),
583 {
584 }
585
587
589 // The older interface for non-modifying access
590 // Not recommended as it will throw an exception if a location has not
591 // been reached in an analysis and there is no (other) way of telling
592 // if a location has been reached.
593 DEPRECATED(SINCE(2019, 08, 01, "use abstract_state_{before,after} instead"))
594 const domainT &operator[](locationt l) const
595 {
597
598 if(p.use_count() == 1)
599 {
600 // Would be unsafe to return the dereferenced object
601 throw std::out_of_range("failed to find state");
602 }
603
604 return static_cast<const domainT &>(*p);
605 }
606
607protected:
608 // Support the legacy get_state interface which is needed for a few domains
609 // This is one of the few users of the legacy get_state(locationt) method
610 // in location_sensitive_storaget.
611 DEPRECATED(SINCE(2019, 08, 01, "use get_state(trace_ptrt p) instead"))
613 {
614 auto &s = dynamic_cast<location_sensitive_storaget &>(*storage);
615 return s.get_state(l, *domain_factory);
616 }
617
619
620private:
623 void dummy(const domainT &s) { const statet &x=s; (void)x; }
624
625 // To keep the old constructor interface we disable logging
627};
628
650template<typename domainT>
651class concurrency_aware_ait:public ait<domainT>
652{
653public:
654 using statet = typename ait<domainT>::statet;
655 using locationt = typename statet::locationt;
656
657 // constructor
659 {
660 }
661 explicit concurrency_aware_ait(std::unique_ptr<ai_domain_factory_baset> &&df)
662 : ait<domainT>(std::move(df))
663 {
664 }
665
666 virtual bool merge_shared(
667 const statet &src,
668 locationt from,
669 locationt to,
670 const namespacet &ns)
671 {
672 statet &dest=this->get_state(to);
673 return static_cast<domainT &>(dest).merge_shared(
674 static_cast<const domainT &>(src), from, to, ns);
675 }
676
677protected:
679
681 ai_baset::trace_ptrt start_trace,
682 const goto_functionst &goto_functions,
683 const namespacet &ns) override
684 {
685 ai_baset::fixedpoint(start_trace, goto_functions, ns);
686
687 is_threadedt is_threaded(goto_functions);
688
689 // construct an initial shared state collecting the results of all
690 // functions
691 goto_programt tmp;
692 tmp.add_instruction();
693 goto_programt::const_targett sh_target = tmp.instructions.begin();
694 ai_baset::trace_ptrt target_hist =
696 statet &shared_state = ait<domainT>::get_state(sh_target);
697
698 struct wl_entryt
699 {
700 wl_entryt(
701 const irep_idt &_function_id,
702 const goto_programt &_goto_program,
703 locationt _location)
704 : function_id(_function_id),
705 goto_program(&_goto_program),
706 location(_location)
707 {
708 }
709
710 irep_idt function_id;
711 const goto_programt *goto_program;
712 locationt location;
713 };
714
715 typedef std::list<wl_entryt> thread_wlt;
716 thread_wlt thread_wl;
717
718 for(const auto &gf_entry : goto_functions.function_map)
719 {
720 forall_goto_program_instructions(t_it, gf_entry.second.body)
721 {
722 if(is_threaded(t_it))
723 {
724 thread_wl.push_back(
725 wl_entryt(gf_entry.first, gf_entry.second.body, t_it));
726
728 gf_entry.second.body.instructions.end();
729 --l_end;
730
731 merge_shared(shared_state, l_end, sh_target, ns);
732 }
733 }
734 }
735
736 // now feed in the shared state into all concurrently executing
737 // functions, and iterate until the shared state stabilizes
738 bool new_shared = true;
739 while(new_shared)
740 {
741 new_shared = false;
742
743 for(const auto &wl_entry : thread_wl)
744 {
745 working_sett working_set;
747 ai_baset::history_factory->epoch(wl_entry.location));
748 ai_baset::put_in_working_set(working_set, t);
749
750 statet &begin_state = ait<domainT>::get_state(wl_entry.location);
751 ait<domainT>::merge(begin_state, target_hist, t);
752
753 while(!working_set.empty())
754 {
756 goto_programt::const_targett l = p->current_location();
757
759 wl_entry.function_id,
760 p,
761 working_set,
762 *(wl_entry.goto_program),
763 goto_functions,
764 ns);
765
766 // the underlying domain must make sure that the final state
767 // carries all possible values; otherwise we would need to
768 // merge over each and every state
769 if(l->is_end_function())
770 new_shared |= merge_shared(shared_state, l, sh_target, ns);
771 }
772 }
773 }
774 }
775};
776
777#endif // CPROVER_ANALYSES_AI_H
Abstract Interpretation Domain.
Abstract Interpretation history.
Abstract Interpretation Storage.
Abstract interface to eager or lazy GOTO models.
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
The common case of history is to only care about where you are now, not how you got there!...
Definition ai_history.h:155
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:118
virtual ~ai_baset()
Definition ai.h:139
virtual cstate_ptrt abstract_state_after(const trace_ptrt &p) const
Definition ai.h:249
xmlt output_xml(const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
Output the abstract states for a single function as XML.
Definition ai.h:380
goto_programt::const_targett locationt
Definition ai.h:125
ai_baset(std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh)
Definition ai.h:127
void operator()(const goto_functionst &goto_functions, const namespacet &ns)
Run abstract interpretation on a whole program.
Definition ai.h:157
virtual ctrace_set_ptrt abstract_traces_after(locationt l) const
Returns all of the histories that have reached the end of the instruction.
Definition ai.h:205
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:267
std::unique_ptr< ai_storage_baset > storage
Definition ai.h:512
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:516
ai_history_baset::trace_sett trace_sett
Definition ai.h:123
jsont output_json(const namespacet &ns, const goto_programt &goto_program) const
Output the abstract states for a single function as JSON.
Definition ai.h:343
void operator()(const irep_idt &function_id, const goto_programt &goto_program, const namespacet &ns)
Run abstract interpretation on a single function.
Definition ai.h:144
virtual ctrace_set_ptrt abstract_traces_before(locationt l) const
Returns all of the histories that have reached the start of the instruction.
Definition ai.h:195
virtual cstate_ptrt abstract_state_after(locationt l) const
Get a copy of the abstract state after the given instruction, without needing to know what kind of do...
Definition ai.h:235
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:328
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
xmlt output_xml(const namespacet &ns, const goto_programt &goto_program) const
Output the abstract states for a single function as XML.
Definition ai.h:372
jsont output_json(const goto_modelt &goto_model) const
Output the abstract states for a whole program as JSON.
Definition ai.h:335
message_handlert & message_handler
Definition ai.h:522
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:520
virtual cstate_ptrt abstract_state_before(const trace_ptrt &p) const
The same interfaces but with histories.
Definition ai.h:244
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:441
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
void operator()(const abstract_goto_modelt &goto_model)
Run abstract interpretation on a whole program.
Definition ai.h:168
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:413
void output(const goto_modelt &goto_model, std::ostream &out) const
Output the abstract states for a whole program.
Definition ai.h:312
virtual void clear()
Reset the abstract state.
Definition ai.h:266
std::unique_ptr< ai_domain_factory_baset > domain_factory
For creating domain objects.
Definition ai.h:495
ai_domain_baset statet
Definition ai.h:120
ai_storage_baset::ctrace_set_ptrt ctrace_set_ptrt
Definition ai.h:124
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:194
xmlt output_xml(const goto_modelt &goto_model) const
Output the abstract states for the whole program as XML.
Definition ai.h:364
jsont output_json(const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
Output the abstract states for a single function as JSON.
Definition ai.h:351
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:229
virtual std::unique_ptr< statet > make_temporary_state(const statet &s)
Make a copy of a state.
Definition ai.h:506
ai_history_baset::trace_ptrt trace_ptrt
Definition ai.h:122
void put_in_working_set(working_sett &working_set, trace_ptrt t)
Definition ai.h:420
trace_ptrt get_next(working_sett &working_set)
Get the next location from the work queue.
Definition ai.cpp:211
trace_sett working_sett
The work queue, sorted using the history's ordering operator.
Definition ai.h:415
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:499
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:222
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
void operator()(const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
Run abstract interpretation on a single function.
Definition ai.h:178
void output(const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const
Output the abstract states for a function.
Definition ai.h:321
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
std::unique_ptr< ai_history_factory_baset > history_factory
For creating history objects.
Definition ai.h:492
virtual void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
Definition ai.cpp:206
ai_storage_baset::cstate_ptrt cstate_ptrt
Definition ai.h:121
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition ai_domain.h:55
virtual std::unique_ptr< statet > copy(const statet &s) const =0
virtual bool merge(statet &dest, const statet &src, trace_ptrt from, trace_ptrt to) const =0
std::shared_ptr< const ai_history_baset > trace_ptrt
History objects are intended to be immutable so they can be shared to reduce memory overhead.
Definition ai_history.h:43
static const trace_ptrt no_caller_history
Definition ai_history.h:121
std::set< trace_ptrt, compare_historyt > trace_sett
Definition ai_history.h:79
virtual ai_history_baset::trace_ptrt epoch(ai_history_baset::locationt)=0
Creates a new history from the given starting point.
An easy factory implementation for histories that don't need parameters.
Definition ai_history.h:255
ai_recursive_interproceduralt(std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh)
Definition ai.h:530
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:539
virtual void clear()
Reset the abstract state.
Definition ai_storage.h:80
virtual statet & get_state(trace_ptrt p, const ai_domain_factory_baset &fac)=0
Look up the analysis state for a given history, instantiating a new domain if required.
virtual cstate_ptrt abstract_state_before(trace_ptrt p, const ai_domain_factory_baset &fac) const =0
Non-modifying access to the stored domains, used in the ai_baset public interface.
std::shared_ptr< const trace_sett > ctrace_set_ptrt
Definition ai_storage.h:54
virtual ctrace_set_ptrt abstract_traces_before(locationt l) const =0
Returns all of the histories that have reached the start of the instruction.
std::shared_ptr< const statet > cstate_ptrt
Definition ai_storage.h:49
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
ait(std::unique_ptr< ai_domain_factory_baset > &&df)
Definition ai.h:576
goto_programt::const_targett locationt
Definition ai.h:586
null_message_handlert no_logging
Definition ai.h:626
void dummy(const domainT &s)
This function exists to enforce that domainT is derived from ai_domain_baset.
Definition ai.h:623
virtual statet & get_state(locationt l)
Definition ai.h:612
ait()
Definition ai.h:566
Base class for concurrency-aware abstract interpretation.
Definition ai.h:652
ai_baset::working_sett working_sett
Definition ai.h:678
typename ait< domainT >::statet statet
Definition ai.h:654
concurrency_aware_ait(std::unique_ptr< ai_domain_factory_baset > &&df)
Definition ai.h:661
virtual bool merge_shared(const statet &src, locationt from, locationt to, const namespacet &ns)
Definition ai.h:666
void fixedpoint(ai_baset::trace_ptrt start_trace, const goto_functionst &goto_functions, const namespacet &ns) override
Definition ai.h:680
typename statet::locationt locationt
Definition ai.h:655
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
targett add_instruction()
Adds an instruction at the end.
Definition json.h:27
The most conventional storage; one domain per location.
Definition ai_storage.h:154
statet & get_state(trace_ptrt p, const ai_domain_factory_baset &fac) override
Look up the analysis state for a given history, instantiating a new domain if required.
Definition ai_storage.h:193
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Definition xml.h:21
#define SINCE(year, month, day, msg)
Definition deprecate.h:26
#define DEPRECATED(msg)
Definition deprecate.h:23
Symbol Table + CFG.
#define forall_goto_program_instructions(it, program)
Over-approximate Concurrency for Threaded Goto Programs.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition make_unique.h:19
STL namespace.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
dstringt irep_idt