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
117
119{
120public:
127
129 std::unique_ptr<ai_history_factory_baset> &&hf,
130 std::unique_ptr<ai_domain_factory_baset> &&df,
131 std::unique_ptr<ai_storage_baset> &&st,
133 : history_factory(std::move(hf)),
134 domain_factory(std::move(df)),
135 storage(std::move(st)),
137 {
138 }
139
140 virtual ~ai_baset()
141 {
142 }
143
146 const irep_idt &function_id,
147 const goto_programt &goto_program,
148 const namespacet &ns)
149 {
150 goto_functionst goto_functions;
151 initialize(function_id, goto_program);
152 trace_ptrt p = entry_state(goto_program);
153 fixedpoint(p, function_id, goto_program, goto_functions, ns);
154 finalize();
155 }
156
159 const goto_functionst &goto_functions,
160 const namespacet &ns)
161 {
162 initialize(goto_functions);
163 trace_ptrt p = entry_state(goto_functions);
164 fixedpoint(p, goto_functions, ns);
165 finalize();
166 }
167
169 void operator()(const abstract_goto_modelt &goto_model)
170 {
171 const namespacet ns(goto_model.get_symbol_table());
172 initialize(goto_model.get_goto_functions());
173 trace_ptrt p = entry_state(goto_model.get_goto_functions());
174 fixedpoint(p, goto_model.get_goto_functions(), ns);
175 finalize();
176 }
177
180 const irep_idt &function_id,
181 const goto_functionst::goto_functiont &goto_function,
182 const namespacet &ns)
183 {
184 goto_functionst goto_functions;
185 initialize(function_id, goto_function);
186 trace_ptrt p = entry_state(goto_function.body);
187 fixedpoint(p, function_id, goto_function.body, goto_functions, ns);
188 finalize();
189 }
190
197 {
198 return storage->abstract_traces_before(l);
199 }
200
207 {
210 INVARIANT(!l->is_end_function(), "No state after the last instruction");
211 return storage->abstract_traces_before(std::next(l));
212 }
213
224 {
225 return storage->abstract_state_before(l, *domain_factory);
226 }
227
237 {
240 INVARIANT(!l->is_end_function(), "No state after the last instruction");
241 return abstract_state_before(std::next(l));
242 }
243
246 {
247 return storage->abstract_state_before(p, *domain_factory);
248 }
249
251 {
252 locationt l = p->current_location();
253 INVARIANT(!l->is_end_function(), "No state after the last instruction");
254
255 locationt n = std::next(l);
256
257 auto step_return = p->step(
258 n,
259 *(storage->abstract_traces_before(n)),
261 // Caller history not needed as this is a local step
262
263 return storage->abstract_state_before(step_return.second, *domain_factory);
264 }
265
267 virtual void clear()
268 {
269 storage->clear();
270 }
271
278 virtual void output(
279 const namespacet &ns,
280 const irep_idt &function_id,
281 const goto_programt &goto_program,
282 std::ostream &out) const;
283
285 virtual void output(
286 const namespacet &ns,
287 const goto_functionst &goto_functions,
288 std::ostream &out) const;
289
291 void output(
292 const goto_modelt &goto_model,
293 std::ostream &out) const
294 {
295 const namespacet ns(goto_model.symbol_table);
296 output(ns, goto_model.goto_functions, out);
297 }
298
300 void output(
301 const namespacet &ns,
302 const goto_functionst::goto_functiont &goto_function,
303 std::ostream &out) const
304 {
305 output(ns, irep_idt(), goto_function.body, out);
306 }
307
309 virtual jsont output_json(
310 const namespacet &ns,
311 const goto_functionst &goto_functions) const;
312
315 const goto_modelt &goto_model) const
316 {
317 const namespacet ns(goto_model.symbol_table);
318 return output_json(ns, goto_model.goto_functions);
319 }
320
323 const namespacet &ns,
324 const goto_programt &goto_program) const
325 {
326 return output_json(ns, irep_idt(), goto_program);
327 }
328
331 const namespacet &ns,
332 const goto_functionst::goto_functiont &goto_function) const
333 {
334 return output_json(ns, irep_idt(), goto_function.body);
335 }
336
338 virtual xmlt output_xml(
339 const namespacet &ns,
340 const goto_functionst &goto_functions) const;
341
344 const goto_modelt &goto_model) const
345 {
346 const namespacet ns(goto_model.symbol_table);
347 return output_xml(ns, goto_model.goto_functions);
348 }
349
352 const namespacet &ns,
353 const goto_programt &goto_program) const
354 {
355 return output_xml(ns, irep_idt(), goto_program);
356 }
357
360 const namespacet &ns,
361 const goto_functionst::goto_functiont &goto_function) const
362 {
363 return output_xml(ns, irep_idt(), goto_function.body);
364 }
365
366protected:
369 virtual void
370 initialize(const irep_idt &function_id, const goto_programt &goto_program);
371
373 virtual void initialize(
374 const irep_idt &function_id,
375 const goto_functionst::goto_functiont &goto_function);
376
379 virtual void initialize(const goto_functionst &goto_functions);
380
383 virtual void finalize();
384
387 trace_ptrt entry_state(const goto_programt &goto_program);
388
391 trace_ptrt entry_state(const goto_functionst &goto_functions);
392
399 virtual jsont output_json(
400 const namespacet &ns,
401 const irep_idt &function_id,
402 const goto_programt &goto_program) const;
403
410 virtual xmlt output_xml(
411 const namespacet &ns,
412 const irep_idt &function_id,
413 const goto_programt &goto_program) const;
414
417
419 trace_ptrt get_next(working_sett &working_set);
420
422 {
423 working_set.insert(t);
424 }
425
428 virtual bool fixedpoint(
429 trace_ptrt starting_trace,
430 const irep_idt &function_id,
431 const goto_programt &goto_program,
432 const goto_functionst &goto_functions,
433 const namespacet &ns);
434
435 virtual void fixedpoint(
436 trace_ptrt starting_trace,
437 const goto_functionst &goto_functions,
438 const namespacet &ns);
439
444 virtual bool visit(
445 const irep_idt &function_id,
446 trace_ptrt p,
447 working_sett &working_set,
448 const goto_programt &goto_program,
449 const goto_functionst &goto_functions,
450 const namespacet &ns);
451
452 // function calls and return are special cases
453 // different kinds of analysis handle these differently so these are virtual
454 // visit_function_call handles which function(s) to call,
455 // while visit_edge_function_call handles a single call
456 virtual bool visit_function_call(
457 const irep_idt &function_id,
458 trace_ptrt p_call,
459 working_sett &working_set,
460 const goto_programt &goto_program,
461 const goto_functionst &goto_functions,
462 const namespacet &ns);
463
464 virtual bool visit_end_function(
465 const irep_idt &function_id,
466 trace_ptrt p,
467 working_sett &working_set,
468 const goto_programt &goto_program,
469 const goto_functionst &goto_functions,
470 const namespacet &ns);
471
472 // The most basic step, computing one edge / transformer application.
473 bool visit_edge(
474 const irep_idt &function_id,
475 trace_ptrt p,
476 const irep_idt &to_function_id,
477 locationt to_l,
478 trace_ptrt caller_history,
479 const namespacet &ns,
480 working_sett &working_set);
481
482 virtual bool visit_edge_function_call(
483 const irep_idt &calling_function_id,
484 trace_ptrt p_call,
485 locationt l_return,
486 const irep_idt &callee_function_id,
487 working_sett &working_set,
488 const goto_programt &callee,
489 const goto_functionst &goto_functions,
490 const namespacet &ns);
491
493 std::unique_ptr<ai_history_factory_baset> history_factory;
494
496 std::unique_ptr<ai_domain_factory_baset> domain_factory;
497
500 virtual bool merge(const statet &src, trace_ptrt from, trace_ptrt to)
501 {
502 statet &dest = get_state(to);
503 return domain_factory->merge(dest, src, from, to);
504 }
505
507 virtual std::unique_ptr<statet> make_temporary_state(const statet &s)
508 {
509 return domain_factory->copy(s);
510 }
511
512 // Domain and history storage
513 std::unique_ptr<ai_storage_baset> storage;
514
518 {
519 return storage->get_state(p, *domain_factory);
520 }
521
522 // Logging
524};
525
526// Perform interprocedural analysis by simply recursing in the interpreter
527// This can lead to a call stack overflow if the domain has a large height
529{
530public:
532 std::unique_ptr<ai_history_factory_baset> &&hf,
533 std::unique_ptr<ai_domain_factory_baset> &&df,
534 std::unique_ptr<ai_storage_baset> &&st,
536 : ai_baset(std::move(hf), std::move(df), std::move(st), mh)
537 {
538 }
539
540protected:
541 // Override the function that handles a single function call edge
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) override;
551};
552
562template <typename domainT>
564{
565public:
566 // constructor
574 {
575 }
576
577 explicit ait(std::unique_ptr<ai_domain_factory_baset> &&df)
581 std::move(df),
584 {
585 }
586
588
590 // The older interface for non-modifying access
591 // Not recommended as it will throw an exception if a location has not
592 // been reached in an analysis and there is no (other) way of telling
593 // if a location has been reached.
594 DEPRECATED(SINCE(2019, 08, 01, "use abstract_state_{before,after} instead"))
595 const domainT &operator[](locationt l) const
596 {
597 auto p = storage->abstract_state_before(l, *domain_factory);
598
599 if(p.use_count() == 1)
600 {
601 // Would be unsafe to return the dereferenced object
602 throw std::out_of_range("failed to find state");
603 }
604
605 return static_cast<const domainT &>(*p);
606 }
607
608protected:
609 // Support the legacy get_state interface which is needed for a few domains
610 // This is one of the few users of the legacy get_state(locationt) method
611 // in location_sensitive_storaget.
612 DEPRECATED(SINCE(2019, 08, 01, "use get_state(trace_ptrt p) instead"))
614 {
615 auto &s = dynamic_cast<location_sensitive_storaget &>(*storage);
616 return s.get_state(l, *domain_factory);
617 }
618
620
621private:
624 void dummy(const domainT &s) { const statet &x=s; (void)x; }
625
626 // To keep the old constructor interface we disable logging
628};
629
651template<typename domainT>
652class concurrency_aware_ait:public ait<domainT>
653{
654public:
655 using statet = typename ait<domainT>::statet;
656 using locationt = typename statet::locationt;
657
658 // constructor
660 {
661 }
662 explicit concurrency_aware_ait(std::unique_ptr<ai_domain_factory_baset> &&df)
663 : ait<domainT>(std::move(df))
664 {
665 }
666
667 virtual bool merge_shared(
668 const statet &src,
669 locationt from,
670 locationt to,
671 const namespacet &ns)
672 {
673 statet &dest=this->get_state(to);
674 return static_cast<domainT &>(dest).merge_shared(
675 static_cast<const domainT &>(src), from, to, ns);
676 }
677
678protected:
680
682 ai_baset::trace_ptrt start_trace,
683 const goto_functionst &goto_functions,
684 const namespacet &ns) override
685 {
686 ai_baset::fixedpoint(start_trace, goto_functions, ns);
687
688 is_threadedt is_threaded(goto_functions);
689
690 // construct an initial shared state collecting the results of all
691 // functions
692 goto_programt tmp;
693 tmp.add_instruction();
694 goto_programt::const_targett sh_target = tmp.instructions.begin();
695 ai_baset::trace_ptrt target_hist =
696 ai_baset::history_factory->epoch(sh_target);
697 statet &shared_state = ait<domainT>::get_state(sh_target);
698
699 struct wl_entryt
700 {
701 wl_entryt(
702 const irep_idt &_function_id,
703 const goto_programt &_goto_program,
704 locationt _location)
705 : function_id(_function_id),
706 goto_program(&_goto_program),
707 location(_location)
708 {
709 }
710
711 irep_idt function_id;
712 const goto_programt *goto_program;
713 locationt location;
714 };
715
716 typedef std::list<wl_entryt> thread_wlt;
717 thread_wlt thread_wl;
718
719 for(const auto &gf_entry : goto_functions.function_map)
720 {
721 forall_goto_program_instructions(t_it, gf_entry.second.body)
722 {
723 if(is_threaded(t_it))
724 {
725 thread_wl.push_back(
726 wl_entryt(gf_entry.first, gf_entry.second.body, t_it));
727
729 gf_entry.second.body.instructions.end();
730 --l_end;
731
732 merge_shared(shared_state, l_end, sh_target, ns);
733 }
734 }
735 }
736
737 // now feed in the shared state into all concurrently executing
738 // functions, and iterate until the shared state stabilizes
739 bool new_shared = true;
740 while(new_shared)
741 {
742 new_shared = false;
743
744 for(const auto &wl_entry : thread_wl)
745 {
746 working_sett working_set;
748 ai_baset::history_factory->epoch(wl_entry.location));
749 ai_baset::put_in_working_set(working_set, t);
750
751 statet &begin_state = ait<domainT>::get_state(wl_entry.location);
752 ait<domainT>::merge(begin_state, target_hist, t);
753
754 while(!working_set.empty())
755 {
757 goto_programt::const_targett l = p->current_location();
758
760 wl_entry.function_id,
761 p,
762 working_set,
763 *(wl_entry.goto_program),
764 goto_functions,
765 ns);
766
767 // the underlying domain must make sure that the final state
768 // carries all possible values; otherwise we would need to
769 // merge over each and every state
770 if(l->is_end_function())
771 new_shared |= merge_shared(shared_state, l, sh_target, ns);
772 }
773 }
774 }
775 }
776};
777
778#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:119
virtual ~ai_baset()
Definition: ai.h:140
virtual cstate_ptrt abstract_state_after(const trace_ptrt &p) const
Definition: ai.h:250
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:359
goto_programt::const_targett locationt
Definition: ai.h:126
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:128
void operator()(const goto_functionst &goto_functions, const namespacet &ns)
Run abstract interpretation on a whole program.
Definition: ai.h:158
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:206
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:262
virtual jsont output_json(const namespacet &ns, const goto_functionst &goto_functions) const
Output the abstract states for the whole program as JSON.
Definition: ai.cpp:60
std::unique_ptr< ai_storage_baset > storage
Definition: ai.h:513
virtual xmlt output_xml(const namespacet &ns, const goto_functionst &goto_functions) const
Output the abstract states for the whole program as XML.
Definition: ai.cpp:107
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:517
ai_history_baset::trace_sett trace_sett
Definition: ai.h:124
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:322
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:145
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:196
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:236
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:323
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:40
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:351
jsont output_json(const goto_modelt &goto_model) const
Output the abstract states for a whole program as JSON.
Definition: ai.h:314
message_handlert & message_handler
Definition: ai.h:523
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:515
virtual cstate_ptrt abstract_state_before(const trace_ptrt &p) const
The same interfaces but with histories.
Definition: ai.h:245
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:436
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:174
void operator()(const abstract_goto_modelt &goto_model)
Run abstract interpretation on a whole program.
Definition: ai.h:169
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:408
void output(const goto_modelt &goto_model, std::ostream &out) const
Output the abstract states for a whole program.
Definition: ai.h:291
virtual void clear()
Reset the abstract state.
Definition: ai.h:267
std::unique_ptr< ai_domain_factory_baset > domain_factory
For creating domain objects.
Definition: ai.h:496
ai_domain_baset statet
Definition: ai.h:121
ai_storage_baset::ctrace_set_ptrt ctrace_set_ptrt
Definition: ai.h:125
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:189
xmlt output_xml(const goto_modelt &goto_model) const
Output the abstract states for the whole program as XML.
Definition: ai.h:343
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:330
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:224
virtual std::unique_ptr< statet > make_temporary_state(const statet &s)
Make a copy of a state.
Definition: ai.h:507
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai.h:123
void put_in_working_set(working_sett &working_set, trace_ptrt t)
Definition: ai.h:421
trace_ptrt get_next(working_sett &working_set)
Get the next location from the work queue.
Definition: ai.cpp:206
trace_sett working_sett
The work queue, sorted using the history's ordering operator.
Definition: ai.h:416
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:500
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:223
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:179
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:300
std::unique_ptr< ai_history_factory_baset > history_factory
For creating history objects.
Definition: ai.h:493
virtual void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
Definition: ai.cpp:201
ai_storage_baset::cstate_ptrt cstate_ptrt
Definition: ai.h:122
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:55
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
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:531
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:534
std::shared_ptr< const trace_sett > ctrace_set_ptrt
Definition: ai_storage.h:54
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:564
ait(std::unique_ptr< ai_domain_factory_baset > &&df)
Definition: ai.h:577
goto_programt::const_targett locationt
Definition: ai.h:587
null_message_handlert no_logging
Definition: ai.h:627
void dummy(const domainT &s)
This function exists to enforce that domainT is derived from ai_domain_baset.
Definition: ai.h:624
virtual statet & get_state(locationt l)
Definition: ai.h:613
ait()
Definition: ai.h:567
Base class for concurrency-aware abstract interpretation.
Definition: ai.h:653
ai_baset::working_sett working_sett
Definition: ai.h:679
typename ait< domainT >::statet statet
Definition: ai.h:655
concurrency_aware_ait(std::unique_ptr< ai_domain_factory_baset > &&df)
Definition: ai.h:662
virtual bool merge_shared(const statet &src, locationt from, locationt to, const namespacet &ns)
Definition: ai.h:667
concurrency_aware_ait()
Definition: ai.h:659
void fixedpoint(ai_baset::trace_ptrt start_trace, const goto_functionst &goto_functions, const namespacet &ns) override
Definition: ai.h:681
typename statet::locationt locationt
Definition: ai.h:656
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
instructionst::const_iterator const_targett
Definition: goto_program.h:593
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:723
Definition: json.h:27
The most conventional storage; one domain per location.
Definition: ai_storage.h:153
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:192
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)
dstringt irep_idt
Definition: irep.h:37
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