Skip to content

Commit b2f3157

Browse files
author
Owen Jones
committed
Address review comments
1 parent 9e0c3ed commit b2f3157

File tree

1 file changed

+23
-12
lines changed

1 file changed

+23
-12
lines changed

src/analyses/ai.h

Lines changed: 23 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -90,19 +90,23 @@ class ai_baset
9090
finalize();
9191
}
9292

93-
/// Get the abstract state before the given instruction, without needing to
94-
/// know what kind of domain or history is used. Note: intended for
95-
/// users of the abstract interpreter; don't use internally.
93+
/// Get a copy of the abstract state before the given instruction, without
94+
/// needing to know what kind of domain or history is used. Note: intended
95+
/// for users of the abstract interpreter; derived classes should
96+
/// use \ref get_state or \ref find_state to access the actual underlying
97+
/// state.
9698
/// PRECONDITION(l is dereferenceable)
9799
/// \param l: The location we want the domain before
98100
/// \return The domain before `l`. We return a pointer to a copy as the method
99101
/// should be const and there are some non-trivial cases including merging
100102
/// domains, etc.
101103
virtual std::unique_ptr<statet> abstract_state_before(locationt l) const = 0;
102104

103-
/// Get the abstract state after the given instruction, without needing to
104-
/// know what kind of domain or history is used. Note: intended for
105-
/// users of the abstract interpreter; don't use internally.
105+
/// Get a copy of the abstract state after the given instruction, without
106+
/// needing to know what kind of domain or history is used. Note: intended
107+
/// for users of the abstract interpreter; derived classes should
108+
/// use \ref get_state or \ref find_state to access the actual underlying
109+
/// state.
106110
/// \param l: The location we want the domain after
107111
/// \return The domain after `l`. We return a pointer to a copy as the method
108112
/// should be const and there are some non-trivial cases including merging
@@ -212,16 +216,15 @@ class ai_baset
212216
}
213217

214218
protected:
215-
/// Initialize all the domains for a single function. Overloaded this to add a
216-
/// factory.
219+
/// Initialize all the domains for a single function. Override this to do
220+
/// custom per-domain initialization.
217221
virtual void initialize(const goto_programt &goto_program);
218222

219-
/// Initialize all the domains for a single function. Overloaded this to add a
220-
/// factory.
223+
/// Initialize all the domains for a single function.
221224
virtual void initialize(const goto_functionst::goto_functiont &goto_function);
222225

223-
/// Initialize all the domains for a whole program. Overloaded this to add a
224-
/// factory.
226+
/// Initialize all the domains for a whole program. Override this to do custom
227+
/// per-analysis initialization.
225228
virtual void initialize(const goto_functionst &goto_functions);
226229

227230
/// Override this to add a cleanup step after fixedpoint has run
@@ -341,8 +344,16 @@ class ai_baset
341344
locationt from,
342345
locationt to,
343346
const namespacet &ns)=0;
347+
348+
/// Get the state for the given location, creating it in a default way if it
349+
/// doesn't exist
344350
virtual statet &get_state(locationt l)=0;
351+
352+
/// Get the state for the given location if it already exists; throw an
353+
/// exception if it doesn't
345354
virtual const statet &find_state(locationt l) const=0;
355+
356+
/// Make a copy of a state
346357
virtual std::unique_ptr<statet> make_temporary_state(const statet &s)=0;
347358
};
348359

0 commit comments

Comments
 (0)