Skip to content

Commit 77237a6

Browse files
author
Daniel Kroening
committed
clean out checks for reference_to expressions
This has no know users.
1 parent 8300e2d commit 77237a6

File tree

6 files changed

+3
-90
lines changed

6 files changed

+3
-90
lines changed

src/analyses/invariant_set.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -134,8 +134,7 @@ std::string inv_object_storet::build_string(const exprt &expr) const
134134
return integer2string(*i);
135135
}
136136

137-
// we also like "address_of" and "reference_to"
138-
// if the object is constant
137+
// we also like "address_of" if the object is constant
139138
// we don't know what mode (language) we are in, so we rely on the default
140139
// language to be reasonable for from_expr
141140
if(is_constant_address(expr))

src/pointer-analysis/goto_program_dereference.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -96,7 +96,7 @@ void goto_program_dereferencet::dereference_failure(
9696
}
9797
}
9898

99-
/// Turn subexpression of `expr` of the form `&*p` or `reference_to(*p)` to p
99+
/// Turn subexpression of `expr` of the form `&*p` into p
100100
/// and use `dereference` on subexpressions of the form `*p`
101101
/// \param expr: expression in which to remove dereferences
102102
/// \param guard: boolean expression assumed to hold when dereferencing
@@ -172,8 +172,7 @@ void goto_program_dereferencet::dereference_rec(
172172
return;
173173
}
174174

175-
if(expr.id()==ID_address_of ||
176-
expr.id()=="reference_to")
175+
if(expr.id() == ID_address_of)
177176
{
178177
// turn &*p to p
179178
// this has *no* side effect!

src/pointer-analysis/value_set.cpp

Lines changed: 0 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -493,31 +493,6 @@ void value_sett::get_value_set_rec(
493493
}
494494
}
495495
}
496-
else if(expr.id()=="reference_to")
497-
{
498-
// old stuff, will go away
499-
object_mapt reference_set;
500-
501-
get_reference_set(expr, reference_set, ns);
502-
503-
const object_map_dt &object_map=reference_set.read();
504-
505-
if(object_map.begin()==object_map.end())
506-
insert(dest, exprt(ID_unknown, original_type));
507-
else
508-
{
509-
for(object_map_dt::const_iterator
510-
it=object_map.begin();
511-
it!=object_map.end();
512-
it++)
513-
{
514-
/// Do not take a reference to object_numbering's storage as we may call
515-
/// object_numbering.number(), which may reallocate it.
516-
const exprt object=object_numbering[it->first];
517-
get_value_set_rec(object, dest, suffix, original_type, ns);
518-
}
519-
}
520-
}
521496
else if(expr.is_constant())
522497
{
523498
// check if NULL

src/pointer-analysis/value_set_fi.cpp

Lines changed: 0 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -499,26 +499,6 @@ void value_set_fit::get_value_set_rec(
499499
return;
500500
}
501501
}
502-
else if(expr.id()=="reference_to")
503-
{
504-
object_mapt reference_set;
505-
506-
get_reference_set_sharing(expr, reference_set, ns);
507-
508-
const object_map_dt &object_map=reference_set.read();
509-
510-
if(object_map.begin()!=object_map.end())
511-
{
512-
forall_objects(it, object_map)
513-
{
514-
const exprt &object=object_numbering[it->first];
515-
get_value_set_rec(object, dest, suffix,
516-
original_type, ns, recursion_set);
517-
}
518-
519-
return;
520-
}
521-
}
522502
else if(expr.is_constant())
523503
{
524504
// check if NULL

src/pointer-analysis/value_set_fivr.cpp

Lines changed: 0 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -615,26 +615,6 @@ void value_set_fivrt::get_value_set_rec(
615615
return;
616616
}
617617
}
618-
else if(expr.id()=="reference_to")
619-
{
620-
object_mapt reference_set;
621-
622-
get_reference_set_sharing(expr, reference_set, ns);
623-
624-
const object_map_dt &object_map=reference_set.read();
625-
626-
if(object_map.begin()!=object_map.end())
627-
{
628-
forall_objects(it, object_map)
629-
{
630-
const exprt &object=object_numbering[it->first];
631-
get_value_set_rec(object, dest, suffix,
632-
original_type, ns, recursion_set);
633-
}
634-
635-
return;
636-
}
637-
}
638618
else if(expr.is_constant())
639619
{
640620
// check if NULL

src/pointer-analysis/value_set_fivrns.cpp

Lines changed: 0 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -405,26 +405,6 @@ void value_set_fivrnst::get_value_set_rec(
405405
return;
406406
}
407407
}
408-
else if(expr.id()=="reference_to")
409-
{
410-
object_mapt reference_set;
411-
412-
get_reference_set(expr, reference_set, ns);
413-
414-
const object_map_dt &object_map=reference_set.read();
415-
416-
if(object_map.begin()!=object_map.end())
417-
{
418-
forall_objects(it, object_map)
419-
{
420-
const exprt &object=object_numbering[it->first];
421-
get_value_set_rec(object, dest, suffix,
422-
original_type, ns);
423-
}
424-
425-
return;
426-
}
427-
}
428408
else if(expr.is_constant())
429409
{
430410
// check if NULL

0 commit comments

Comments
 (0)