Skip to content

Commit a5b390d

Browse files
martinmartin
authored andcommitted
Add a typedef for "a pointer to a domain" to simplify interfaces
These are used because it allows const analysers / ai_storage objects to generate new (bottom) domains, so on-the-fly domain creation is properly supported.
1 parent bf96a08 commit a5b390d

File tree

2 files changed

+12
-9
lines changed

2 files changed

+12
-9
lines changed

src/analyses/ai.h

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@ class ai_baset
3535
{
3636
public:
3737
typedef ai_domain_baset statet;
38+
typedef ai_storage_baset::state_ptrt state_ptrt;
3839
typedef goto_programt::const_targett locationt;
3940

4041
ai_baset(
@@ -104,7 +105,7 @@ class ai_baset
104105
/// \return The abstract state before `l`. We return a pointer to a copy as
105106
/// the method should be const and there are some non-trivial cases
106107
/// including merging abstract states, etc.
107-
virtual std::shared_ptr<const statet> abstract_state_before(locationt l) const
108+
virtual state_ptr abstract_state_before(locationt l) const
108109
{
109110
return storage->abstract_state_before(l, *domain_factory);
110111
}
@@ -117,7 +118,7 @@ class ai_baset
117118
/// \return The abstract state after `l`. We return a pointer to a copy as
118119
/// the method should be const and there are some non-trivial cases
119120
/// including merging abstract states, etc.
120-
virtual std::shared_ptr<const statet> abstract_state_after(locationt l) const
121+
virtual state_ptr abstract_state_after(locationt l) const
121122
{
122123
/// PRECONDITION(l is dereferenceable && std::next(l) is dereferenceable)
123124
/// Check relies on a DATA_INVARIANT of goto_programs

src/analyses/ai_storage.h

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -36,12 +36,13 @@ class ai_storage_baset
3636
}
3737

3838
typedef ai_domain_baset statet;
39+
typedef std::shared_ptr<const statet> state_ptrt;
3940
typedef goto_programt::const_targett locationt;
4041

4142
/// Non-modifying access to the stored domains,
4243
/// used in the ai_baset public interface.
4344
/// In the case of un-analysed locals this should create a domain
44-
virtual std::shared_ptr<const statet> abstract_state_before(
45+
virtual statet_ptr abstract_state_before(
4546
locationt l,
4647
const ai_domain_factory_baset &fac) const = 0;
4748

@@ -74,12 +75,13 @@ class dependence_grapht;
7475
class location_sensitive_storaget : public ai_storage_baset
7576
{
7677
protected:
77-
typedef std::shared_ptr<statet> s_ptrt;
78-
7978
/// This is location sensitive so we store one domain per location
80-
typedef std::
81-
unordered_map<locationt, s_ptrt, const_target_hash, pointee_address_equalt>
82-
state_mapt;
79+
typedef std::unordered_map<
80+
locationt,
81+
state_ptrt,
82+
const_target_hash,
83+
pointee_address_equalt>
84+
state_mapt;
8385
state_mapt state_map;
8486

8587
// Support some older domains that explicitly iterate across the state map
@@ -91,7 +93,7 @@ class location_sensitive_storaget : public ai_storage_baset
9193
}
9294

9395
public:
94-
std::shared_ptr<const statet> abstract_state_before(
96+
state_ptrt abstract_state_before(
9597
locationt l,
9698
const ai_domain_factory_baset &fac) const override
9799
{

0 commit comments

Comments
 (0)