Skip to content

Commit eef32db

Browse files
author
martin
committed
Methods for ai_baset to allow access to the ai_base_domaint for a location.
Previously, to access the domain for at a particular location, you had to use the operator[] interface in ait<domainT> (or subclass), which meant that the code had to be written / templated / duplicated for each domainT, even when the only interface that was being used was the ai_base_domaint one. This is the case for various tasks in goto-analyzer. This interface should also support flow-insensitive or context-dependent AI engines.
1 parent aae984a commit eef32db

File tree

1 file changed

+17
-0
lines changed

1 file changed

+17
-0
lines changed

src/analyses/ai.h

+17
Original file line numberDiff line numberDiff line change
@@ -162,6 +162,17 @@ class ai_baset
162162
fixedpoint(goto_function.body, goto_functions, ns);
163163
}
164164

165+
/// Returns the abstract state before the given instruction
166+
virtual const ai_domain_baset & abstract_state_before(
167+
goto_programt::const_targett t) const = 0;
168+
169+
/// Returns the abstract state after the given instruction
170+
virtual const ai_domain_baset & abstract_state_after(
171+
goto_programt::const_targett t) const
172+
{
173+
return abstract_state_before(std::next(t));
174+
}
175+
165176
virtual void clear()
166177
{
167178
}
@@ -370,6 +381,12 @@ class ait:public ai_baset
370381
return it->second;
371382
}
372383

384+
const ai_domain_baset & abstract_state_before(
385+
goto_programt::const_targett t) const override
386+
{
387+
return (*this)[t];
388+
}
389+
373390
void clear() override
374391
{
375392
state_map.clear();

0 commit comments

Comments
 (0)