Skip to content

Commit 837857c

Browse files
author
Owen Jones
committed
Set declared_on_type for precise EVSs
This is in entryt, and its close relative fieldnamet. We now make sure it is well-defined by always setting it to one special value.
1 parent 6dc16bb commit 837857c

File tree

2 files changed

+17
-7
lines changed

2 files changed

+17
-7
lines changed

src/pointer-analysis/external_value_set_expr.h

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -294,6 +294,12 @@ class external_value_set_exprt:public exprt
294294
return copy;
295295
}
296296
}
297+
298+
static const typet &get_precise_evs_irep_id()
299+
{
300+
static typet precise_evs("precise_evs");
301+
return precise_evs;
302+
}
297303
};
298304

299305
inline external_value_set_exprt &to_external_value_set(exprt &e)

src/pointer-analysis/local_value_set.cpp

Lines changed: 11 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -45,12 +45,13 @@ local_value_sett::init_per_field_external_value_set(
4545
const external_value_set_exprt &evse)
4646
{
4747
PRECONDITION(!evse.access_path_entries().empty());
48-
const auto &apback=evse.access_path_entries().back();
49-
std::string basename=evse.get_access_path_basename(apback.declared_on_type());
48+
const typet &declared_on_type =
49+
evse.access_path_entries().back().declared_on_type();
50+
std::string basename = evse.get_access_path_basename(declared_on_type);
5051
std::string access_path_suffix=evse.get_access_path_suffix();
5152
std::string entryname=basename+access_path_suffix;
5253

53-
entryt entry(basename, access_path_suffix, apback.declared_on_type(), evse);
54+
entryt entry(basename, access_path_suffix, declared_on_type, evse);
5455

5556
auto insert_result=values.insert(std::make_pair(irep_idt(entryname), entry));
5657

@@ -65,9 +66,9 @@ void local_value_sett::init_precise_external_value_set(
6566
object_mapt &dest)
6667
{
6768
PRECONDITION(!evse.access_path_entries().empty());
68-
const auto &apback = evse.access_path_entries().back();
69-
std::string basename =
70-
evse.get_access_path_basename(apback.declared_on_type());
69+
const typet &declared_on_type =
70+
external_value_set_exprt::get_precise_evs_irep_id();
71+
std::string basename = evse.get_access_path_basename(declared_on_type);
7172
std::string access_path_suffix = evse.get_access_path_suffix();
7273
std::string entryname = basename + access_path_suffix;
7374

@@ -624,7 +625,10 @@ void local_value_sett::assign_rec(
624625
std::string entryname=basename+access_path_suffix;
625626

626627
entryt entry(
627-
basename, access_path_suffix, declared_on_type, new_ext_set);
628+
basename,
629+
access_path_suffix,
630+
external_value_set_exprt::get_precise_evs_irep_id(),
631+
new_ext_set);
628632

629633
auto insert_result=const_cast<valuest &>(values).
630634
insert(std::make_pair(irep_idt(entryname), entry));

0 commit comments

Comments
 (0)