cprover
Loading...
Searching...
No Matches
reaching_definitions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Range-based reaching definitions analysis (following Field-
4 Sensitive Program Dependence Analysis, Litvak et al., FSE 2010)
5
6Author: Michael Tautschnig
7
8Date: February 2013
9
10\*******************************************************************/
11
15
17
18#include <memory>
19
21#include <util/make_unique.h>
23
25
26#include "is_threaded.h"
27#include "dirty.h"
28
32class rd_range_domain_factoryt : public ai_domain_factoryt<rd_range_domaint>
33{
34public:
37 : bv_container(_bv_container)
38 {
39 PRECONDITION(bv_container != nullptr);
40 }
41
42 std::unique_ptr<statet> make(locationt) const override
43 {
44 auto p = util_make_unique<rd_range_domaint>(bv_container);
45 CHECK_RETURN(p->is_bottom());
46 return std::unique_ptr<statet>(p.release());
47 }
48
49private:
51};
52
54 const namespacet &_ns)
57 ns(_ns)
58{
59}
60
62
71void rd_range_domaint::populate_cache(const irep_idt &identifier) const
72{
73 assert(bv_container);
74
75 valuest::const_iterator v_entry=values.find(identifier);
76 if(v_entry==values.end() ||
77 v_entry->second.empty())
78 return;
79
80 ranges_at_loct &export_entry=export_cache[identifier];
81
82 for(const auto &id : v_entry->second)
83 {
85
86 export_entry[v.definition_at].insert(
87 std::make_pair(v.bit_begin, v.bit_end));
88 }
89}
90
92 const irep_idt &function_from,
93 trace_ptrt trace_from,
94 const irep_idt &function_to,
95 trace_ptrt trace_to,
96 ai_baset &ai,
97 const namespacet &ns)
98{
99 locationt from{trace_from->current_location()};
100 locationt to{trace_to->current_location()};
101
103 dynamic_cast<reaching_definitions_analysist*>(&ai);
105 rd!=nullptr,
107 "ai has type reaching_definitions_analysist");
108
109 assert(bv_container);
110
111 // kill values
112 if(from->is_dead())
113 transform_dead(ns, from);
114 // kill thread-local values
115 else if(from->is_start_thread())
116 transform_start_thread(ns, *rd);
117 // do argument-to-parameter assignments
118 else if(from->is_function_call())
119 transform_function_call(ns, function_from, from, function_to, *rd);
120 // cleanup parameters
121 else if(from->is_end_function())
122 transform_end_function(ns, function_from, from, function_to, to, *rd);
123 // lhs assignments
124 else if(from->is_assign())
125 transform_assign(ns, from, function_from, from, *rd);
126 // initial (non-deterministic) value
127 else if(from->is_decl())
128 transform_assign(ns, from, function_from, from, *rd);
129
130#if 0
131 // handle return values
132 if(to->is_function_call())
133 {
134 const code_function_callt &code=to_code_function_call(to->code);
135
136 if(code.lhs().is_not_nil())
137 {
138 rw_range_set_value_sett rw_set(ns, rd->get_value_sets());
139 goto_rw(to, rw_set);
140 const bool is_must_alias=rw_set.get_w_set().size()==1;
141
142 for(const auto &written_object_entry : rw_set.get_w_set())
143 {
144 const irep_idt &identifier = written_object_entry.first;
145 // ignore symex::invalid_object
146 const symbolt *symbol_ptr;
147 if(ns.lookup(identifier, symbol_ptr))
148 continue;
149 assert(symbol_ptr!=0);
150
151 const range_domaint &ranges =
152 rw_set.get_ranges(written_object_entry.second);
153
154 if(is_must_alias &&
155 (!rd->get_is_threaded()(from) ||
156 (!symbol_ptr->is_shared() &&
157 !rd->get_is_dirty()(identifier))))
158 for(const auto &range : ranges)
159 kill(identifier, range.first, range.second);
160 }
161 }
162 }
163#endif
164}
165
169 const namespacet &,
170 locationt from)
171{
172 const irep_idt &identifier = from->dead_symbol().get_identifier();
173
174 valuest::iterator entry=values.find(identifier);
175
176 if(entry!=values.end())
177 {
178 values.erase(entry);
179 export_cache.erase(identifier);
180 }
181}
182
184 const namespacet &ns,
186{
187 for(valuest::iterator it=values.begin();
188 it!=values.end();
189 ) // no ++it
190 {
191 const irep_idt &identifier=it->first;
192
193 if(!ns.lookup(identifier).is_shared() &&
194 !rd.get_is_dirty()(identifier))
195 {
196 export_cache.erase(identifier);
197
198 valuest::iterator next=it;
199 ++next;
200 values.erase(it);
201 it=next;
202 }
203 else
204 ++it;
205 }
206}
207
209 const namespacet &ns,
210 const irep_idt &function_from,
211 locationt from,
212 const irep_idt &function_to,
214{
215 // only if there is an actual call, i.e., we have a body
216 if(function_from != function_to)
217 {
218 for(valuest::iterator it=values.begin();
219 it!=values.end();
220 ) // no ++it
221 {
222 const irep_idt &identifier=it->first;
223
224 // dereferencing may introduce extra symbols
225 const symbolt *sym;
226 if((ns.lookup(identifier, sym) ||
227 !sym->is_shared()) &&
228 !rd.get_is_dirty()(identifier))
229 {
230 export_cache.erase(identifier);
231
232 valuest::iterator next=it;
233 ++next;
234 values.erase(it);
235 it=next;
236 }
237 else
238 ++it;
239 }
240
241 const symbol_exprt &fn_symbol_expr = to_symbol_expr(from->call_function());
242 const code_typet &code_type=
243 to_code_type(ns.lookup(fn_symbol_expr.get_identifier()).type);
244
245 for(const auto &param : code_type.parameters())
246 {
247 const irep_idt &identifier=param.get_identifier();
248
249 if(identifier.empty())
250 continue;
251
252 auto param_bits = pointer_offset_bits(param.type(), ns);
253 if(param_bits.has_value())
254 gen(from, identifier, 0, to_range_spect(*param_bits));
255 else
256 gen(from, identifier, 0, -1);
257 }
258 }
259 else
260 {
261 // handle return values of undefined functions
262 if(from->call_lhs().is_not_nil())
263 transform_assign(ns, from, function_from, from, rd);
264 }
265}
266
268 const namespacet &ns,
269 const irep_idt &function_from,
270 locationt from,
271 const irep_idt &function_to,
272 locationt to,
274{
275 locationt call = to;
276 --call;
277
278 valuest new_values;
279 new_values.swap(values);
280 values=rd[call].values;
281
282 for(const auto &new_value : new_values)
283 {
284 const irep_idt &identifier=new_value.first;
285
286 if(!rd.get_is_threaded()(call) ||
287 (!ns.lookup(identifier).is_shared() &&
288 !rd.get_is_dirty()(identifier)))
289 {
290 for(const auto &id : new_value.second)
291 {
294 }
295 }
296
297 for(const auto &id : new_value.second)
298 {
301 }
302 }
303
304 const code_typet &code_type = to_code_type(ns.lookup(function_from).type);
305
306 for(const auto &param : code_type.parameters())
307 {
308 const irep_idt &identifier=param.get_identifier();
309
310 if(identifier.empty())
311 continue;
312
313 valuest::iterator entry=values.find(identifier);
314
315 if(entry!=values.end())
316 {
317 values.erase(entry);
318 export_cache.erase(identifier);
319 }
320 }
321
322 // handle return values
323 if(call->call_lhs().is_not_nil())
324 {
325#if 0
326 rd_range_domaint *rd_state=
327 dynamic_cast<rd_range_domaint*>(&(rd.get_state(call)));
328 assert(rd_state!=0);
329 rd_state->
330#endif
331 transform_assign(ns, from, function_to, call, rd);
332 }
333}
334
336 const namespacet &ns,
337 locationt from,
338 const irep_idt &function_to,
339 locationt to,
341{
343 goto_rw(function_to, to, rw_set);
344 const bool is_must_alias=rw_set.get_w_set().size()==1;
345
346 for(const auto &written_object_entry : rw_set.get_w_set())
347 {
348 const irep_idt &identifier = written_object_entry.first;
349 // ignore symex::invalid_object
350 const symbolt *symbol_ptr;
351 if(ns.lookup(identifier, symbol_ptr))
352 continue;
354 symbol_ptr!=nullptr,
356 "Symbol is in symbol table");
357
358 const range_domaint &ranges =
359 rw_set.get_ranges(written_object_entry.second);
360
361 if(is_must_alias &&
362 (!rd.get_is_threaded()(from) ||
363 (!symbol_ptr->is_shared() &&
364 !rd.get_is_dirty()(identifier))))
365 for(const auto &range : ranges)
366 kill(identifier, range.first, range.second);
367
368 for(const auto &range : ranges)
369 gen(from, identifier, range.first, range.second);
370 }
371}
372
374 const irep_idt &identifier,
375 const range_spect &range_start,
376 const range_spect &range_end)
377{
378 assert(range_start>=0);
379 // -1 for objects of infinite/unknown size
380 if(range_end==-1)
381 {
382 kill_inf(identifier, range_start);
383 return;
384 }
385
386 assert(range_end>range_start);
387
388 valuest::iterator entry=values.find(identifier);
389 if(entry==values.end())
390 return;
391
392 bool clear_export_cache=false;
393 values_innert new_values;
394
395 for(values_innert::iterator
396 it=entry->second.begin();
397 it!=entry->second.end();
398 ) // no ++it
399 {
401
402 if(v.bit_begin >= range_end)
403 ++it;
404 else if(v.bit_end!=-1 &&
405 v.bit_end <= range_start)
406 ++it;
407 else if(v.bit_begin >= range_start &&
408 v.bit_end!=-1 &&
409 v.bit_end <= range_end) // rs <= a < b <= re
410 {
411 clear_export_cache=true;
412
413 entry->second.erase(it++);
414 }
415 else if(v.bit_begin >= range_start) // rs <= a <= re < b
416 {
417 clear_export_cache=true;
418
419 reaching_definitiont v_new=v;
420 v_new.bit_begin=range_end;
421 new_values.insert(bv_container->add(v_new));
422
423 entry->second.erase(it++);
424 }
425 else if(v.bit_end==-1 ||
426 v.bit_end > range_end) // a <= rs < re < b
427 {
428 clear_export_cache=true;
429
430 reaching_definitiont v_new=v;
431 v_new.bit_end=range_start;
432
433 reaching_definitiont v_new2=v;
434 v_new2.bit_begin=range_end;
435
436 new_values.insert(bv_container->add(v_new));
437 new_values.insert(bv_container->add(v_new2));
438
439 entry->second.erase(it++);
440 }
441 else // a <= rs < b <= re
442 {
443 clear_export_cache=true;
444
445 reaching_definitiont v_new=v;
446 v_new.bit_end=range_start;
447 new_values.insert(bv_container->add(v_new));
448
449 entry->second.erase(it++);
450 }
451 }
452
453 if(clear_export_cache)
454 export_cache.erase(identifier);
455
456 values_innert::iterator it=entry->second.begin();
457 for(const auto &id : new_values)
458 {
459 while(it!=entry->second.end() && *it<id)
460 ++it;
461 if(it==entry->second.end() || id<*it)
462 {
463 entry->second.insert(it, id);
464 }
465 else if(it!=entry->second.end())
466 {
467 assert(*it==id);
468 ++it;
469 }
470 }
471}
472
474 const irep_idt &,
475 const range_spect &range_start)
476{
477 assert(range_start>=0);
478
479#if 0
480 valuest::iterator entry=values.find(identifier);
481 if(entry==values.end())
482 return;
483
484 XXX export_cache_available=false;
485
486 // makes the analysis underapproximating
487 rangest &ranges=entry->second;
488
489 for(rangest::iterator it=ranges.begin();
490 it!=ranges.end();
491 ) // no ++it
492 if(it->second.first!=-1 &&
493 it->second.first <= range_start)
494 ++it;
495 else if(it->first >= range_start) // rs <= a < b <= re
496 {
497 ranges.erase(it++);
498 }
499 else // a <= rs < b < re
500 {
501 it->second.first=range_start;
502 ++it;
503 }
504#endif
505}
506
512 locationt from,
513 const irep_idt &identifier,
514 const range_spect &range_start,
515 const range_spect &range_end)
516{
517 // objects of size 0 like union U { signed : 0; };
518 if(range_start==0 && range_end==0)
519 return false;
520
521 assert(range_start>=0);
522
523 // -1 for objects of infinite/unknown size
524 assert(range_end>range_start || range_end==-1);
525
527 v.identifier=identifier;
528 v.definition_at=from;
529 v.bit_begin=range_start;
530 v.bit_end=range_end;
531
532 if(!values[identifier].insert(bv_container->add(v)).second)
533 return false;
534
535 export_cache.erase(identifier);
536
537#if 0
538 range_spect merged_range_end=range_end;
539
540 std::pair<valuest::iterator, bool> entry=
541 values.insert(std::make_pair(identifier, rangest()));
542 rangest &ranges=entry.first->second;
543
544 if(!entry.second)
545 {
546 for(rangest::iterator it=ranges.begin();
547 it!=ranges.end();
548 ) // no ++it
549 {
550 if(it->second.second!=from ||
551 (it->second.first!=-1 && it->second.first <= range_start) ||
552 (range_end!=-1 && it->first >= range_end))
553 ++it;
554 else if(it->first > range_start) // rs < a < b,re
555 {
556 if(range_end!=-1)
557 merged_range_end=std::max(range_end, it->second.first);
558 ranges.erase(it++);
559 }
560 else if(it->second.first==-1 ||
561 (range_end!=-1 &&
562 it->second.first >= range_end)) // a <= rs < re <= b
563 {
564 // nothing to do
565 return false;
566 }
567 else // a <= rs < b < re
568 {
569 it->second.first=range_end;
570 return true;
571 }
572 }
573 }
574
575 ranges.insert(std::make_pair(
576 range_start,
577 std::make_pair(merged_range_end, from)));
578#endif
579
580 return true;
581}
582
583void rd_range_domaint::output(std::ostream &out) const
584{
585 out << "Reaching definitions:\n";
586
587 if(has_values.is_known())
588 {
589 out << has_values.to_string() << '\n';
590 return;
591 }
592
593 for(const auto &value : values)
594 {
595 const irep_idt &identifier=value.first;
596
597 const ranges_at_loct &ranges=get(identifier);
598
599 out << " " << identifier << "[";
600
601 for(ranges_at_loct::const_iterator itl=ranges.begin();
602 itl!=ranges.end();
603 ++itl)
604 for(rangest::const_iterator itr=itl->second.begin();
605 itr!=itl->second.end();
606 ++itr)
607 {
608 if(itr!=itl->second.begin() ||
609 itl!=ranges.begin())
610 out << ";";
611
612 out << itr->first << ":" << itr->second;
613 out << "@" << itl->first->location_number;
614 }
615
616 out << "]\n";
617
618 clear_cache(identifier);
619 }
620}
621
624 values_innert &dest,
625 const values_innert &other)
626{
627 bool more=false;
628
629#if 0
630 ranges_at_loct::iterator itr=it->second.begin();
631 for(const auto &o : ito->second)
632 {
633 while(itr!=it->second.end() && itr->first<o.first)
634 ++itr;
635 if(itr==it->second.end() || o.first<itr->first)
636 {
637 it->second.insert(o);
638 more=true;
639 }
640 else if(itr!=it->second.end())
641 {
642 assert(itr->first==o.first);
643
644 for(const auto &o_range : o.second)
645 more=gen(itr->second, o_range.first, o_range.second) ||
646 more;
647
648 ++itr;
649 }
650 }
651#else
652 values_innert::iterator itr=dest.begin();
653 for(const auto &id : other)
654 {
655 while(itr!=dest.end() && *itr<id)
656 ++itr;
657 if(itr==dest.end() || id<*itr)
658 {
659 dest.insert(itr, id);
660 more=true;
661 }
662 else if(itr!=dest.end())
663 {
664 assert(*itr==id);
665 ++itr;
666 }
667 }
668#endif
669
670 return more;
671}
672
674 const rd_range_domaint &other,
677{
678 bool changed=has_values.is_false();
680
681 valuest::iterator it=values.begin();
682 for(const auto &value : other.values)
683 {
684 while(it!=values.end() && it->first<value.first)
685 ++it;
686 if(it==values.end() || value.first<it->first)
687 {
688 values.insert(value);
689 changed=true;
690 }
691 else if(it!=values.end())
692 {
693 assert(it->first==value.first);
694
695 if(merge_inner(it->second, value.second))
696 {
697 changed=true;
698 export_cache.erase(it->first);
699 }
700
701 ++it;
702 }
703 }
704
705 return changed;
706}
707
710 const rd_range_domaint &other,
711 locationt,
712 locationt,
713 const namespacet &ns)
714{
715 // TODO: dirty vars
716#if 0
718 dynamic_cast<reaching_definitions_analysist*>(&ai);
719 assert(rd!=0);
720#endif
721
722 bool changed=has_values.is_false();
724
725 valuest::iterator it=values.begin();
726 for(const auto &value : other.values)
727 {
728 const irep_idt &identifier=value.first;
729
730 if(!ns.lookup(identifier).is_shared()
731 /*&& !rd.get_is_dirty()(identifier)*/)
732 continue;
733
734 while(it!=values.end() && it->first<value.first)
735 ++it;
736 if(it==values.end() || value.first<it->first)
737 {
738 values.insert(value);
739 changed=true;
740 }
741 else if(it!=values.end())
742 {
743 assert(it->first==value.first);
744
745 if(merge_inner(it->second, value.second))
746 {
747 changed=true;
748 export_cache.erase(it->first);
749 }
750
751 ++it;
752 }
753 }
754
755 return changed;
756}
757
759 const irep_idt &identifier) const
760{
761 populate_cache(identifier);
762
763 static ranges_at_loct empty;
764
765 export_cachet::const_iterator entry=export_cache.find(identifier);
766
767 if(entry==export_cache.end())
768 return empty;
769 else
770 return entry->second;
771}
772
774 const goto_functionst &goto_functions)
775{
776 auto value_sets_=util_make_unique<value_set_analysis_fit>(ns);
777 (*value_sets_)(goto_functions);
778 value_sets=std::move(value_sets_);
779
780 is_threaded=util_make_unique<is_threadedt>(goto_functions);
781
782 is_dirty=util_make_unique<dirtyt>(goto_functions);
783
785}
Generic exception types primarily designed for use with invariants.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
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
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:74
goto_programt::const_targett locationt
Definition: ai_domain.h:73
ai_domain_factory_baset::locationt locationt
Definition: ai_domain.h:200
virtual statet & get_state(locationt l)
Definition: ai.h:613
codet representation of a function call statement.
Base type of functions.
Definition: std_types.h:539
const parameterst & parameters() const
Definition: std_types.h:655
Base class for concurrency-aware abstract interpretation.
Definition: ai.h:653
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
A collection of goto functions.
bool is_not_nil() const
Definition: irep.h:380
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
This ensures that all domains are constructed with the appropriate pointer back to the analysis engin...
std::unique_ptr< statet > make(locationt) const override
sparse_bitvector_analysist< reaching_definitiont > *const bv_container
rd_range_domain_factoryt(sparse_bitvector_analysist< reaching_definitiont > *_bv_container)
Because the class is inherited from ai_domain_baset, its instance represents an element of a domain o...
void populate_cache(const irep_idt &identifier) const
Given the passed variable name identifier it collects data from bv_container for each ID in values[id...
export_cachet export_cache
It is a helper data structure.
void output(std::ostream &out, const ai_baset &, const namespacet &) const final override
void kill_inf(const irep_idt &identifier, const range_spect &range_start)
void transform_dead(const namespacet &ns, locationt from)
Computes an instance obtained from a *this by transformation over DEAD v GOTO instruction.
void transform_start_thread(const namespacet &ns, reaching_definitions_analysist &rd)
const ranges_at_loct & get(const irep_idt &identifier) const
void clear_cache(const irep_idt &identifier) const
sparse_bitvector_analysist< reaching_definitiont > *const bv_container
It points to the actual reaching definitions data of individual program variables.
void transform_function_call(const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, reaching_definitions_analysist &rd)
bool merge(const rd_range_domaint &other, trace_ptrt from, trace_ptrt to)
Implements the "join" operation of two instances *this and other.
void transform_end_function(const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, reaching_definitions_analysist &rd)
std::map< locationt, rangest > ranges_at_loct
void transform_assign(const namespacet &ns, locationt from, const irep_idt &function_to, locationt to, reaching_definitions_analysist &rd)
bool merge_inner(values_innert &dest, const values_innert &other)
std::multimap< range_spect, range_spect > rangest
bool gen(locationt from, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
A utility function which updates internal data structures by inserting a new reaching definition reco...
void kill(const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
tvt has_values
This (three value logic) flag determines, whether the instance represents top, bottom,...
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override
Computes an instance obtained from the instance *this by transformation over a GOTO instruction refer...
std::map< irep_idt, values_innert > valuest
valuest values
It is an ordered map from program variable names to IDs of reaching_definitiont instances stored in m...
bool merge_shared(const rd_range_domaint &other, locationt from, locationt to, const namespacet &ns)
std::set< std::size_t > values_innert
value_setst & get_value_sets() const
std::unique_ptr< is_threadedt > is_threaded
reaching_definitions_analysist(const namespacet &_ns)
const dirtyt & get_is_dirty() const
const is_threadedt & get_is_threaded() const
std::unique_ptr< dirtyt > is_dirty
std::unique_ptr< value_setst > value_sets
void initialize(const goto_functionst &goto_functions) override
Initialize all the abstract states for a whole program.
const objectst & get_w_set() const
Definition: goto_rw.h:120
const range_domaint & get_ranges(const std::unique_ptr< range_domain_baset > &ranges) const
Definition: goto_rw.h:126
An instance of this class provides an assignment of unique numeric ID to each inserted reaching_defin...
const V & get(const std::size_t value_index) const
std::vector< typename inner_mapt::const_iterator > values
It is a map from an ID to the corresponding reaching_definitiont instance inside the map value_map.
std::size_t add(const V &value)
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
Symbol table entry.
Definition: symbol.h:28
bool is_shared() const
Definition: symbol.h:95
bool is_known() const
Definition: threeval.h:28
const char * to_string() const
Definition: threeval.cpp:13
bool is_false() const
Definition: threeval.h:26
static tvt unknown()
Definition: threeval.h:33
Variables whose address is taken.
const code_function_callt & to_code_function_call(const codet &code)
static void goto_rw(const irep_idt &function, goto_programt::const_targett target, const exprt &lhs, const exprt &function_expr, const exprt::operandst &arguments, rw_range_sett &rw_set)
Definition: goto_rw.cpp:733
int range_spect
Definition: goto_rw.h:57
range_spect to_range_spect(const mp_integer &size)
Definition: goto_rw.h:59
Over-approximate Concurrency for Threaded Goto Programs.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis,...
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:407
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
Identifies a GOTO instruction where a given variable is defined (i.e.
range_spect bit_begin
The two integers below define a range of bits (i.e.
ai_domain_baset::locationt definition_at
The iterator to the GOTO instruction where the variable has been written to.
irep_idt identifier
The name of the variable which was defined.
Value Set Propagation (flow insensitive)