Skip to content

Commit

Permalink
Document the invariants on iterators arguments to transform and merge.
Browse files Browse the repository at this point in the history
In many, but not all, cases they are comparable.  However they should
always be dereferenceable.
  • Loading branch information
martin committed Feb 9, 2018
1 parent e3db794 commit d447c26
Showing 1 changed file with 14 additions and 0 deletions.
14 changes: 14 additions & 0 deletions src/analyses/ai.h
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,15 @@ class ai_domain_baset
// b) there is an edge from the last instruction (END_FUNCTION)
// of the function to the instruction _following_ the call site
// (this also needs to set the LHS, if applicable)
//
// "this" is the domain before the instruction "from"
// "from" is the instruction to be interpretted
// "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)
//
// PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
// PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")
// PRECONDITION(are_comparable(from,to) ||
// (from->is_function_call() || from->is_end_function())

virtual void transform(
locationt from,
Expand Down Expand Up @@ -90,6 +99,11 @@ class ai_domain_baset
//
// This computes the join between "this" and "b".
// Return true if "this" has changed.
// In the usual case, "b" is the updated state after "from"
// and "this" is the state before "to".
//
// PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
// PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")

// This method allows an expression to be simplified / evaluated using the
// current state. It is used to evaluate assertions and in program
Expand Down

0 comments on commit d447c26

Please sign in to comment.