Skip to content

Commit

Permalink
Added missing documentation in Pentagons.java and UpperBounds.java
Browse files Browse the repository at this point in the history
  • Loading branch information
olivieriluca committed Jan 10, 2024
1 parent a797a9a commit ebda88b
Show file tree
Hide file tree
Showing 2 changed files with 71 additions and 0 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -29,16 +29,41 @@
import it.unive.lisa.util.representation.StringRepresentation;
import it.unive.lisa.util.representation.StructuredRepresentation;

/**
* The pentagons abstract domain, a weakly relational numerical abstract domain. This abstract
* domain captures properties of the form of x ⋲ [a, b] ∧ x < y. It is more precise than the
* well known interval domain, but it is less precise than the octagon domain.
* It is implemented as a {@link ValueDomain}.
*
* @author <a href="mailto:[email protected]">Luca Negrini</a>
* @author <a href="mailto:[email protected]">Vincenzo Arceri</a>
*/
public class Pentagons implements ValueDomain<Pentagons>, BaseLattice<Pentagons> {

/**
* The interval environment.
*/
private final ValueEnvironment<Interval> intervals;

/**
* The upper bounds environment.
*/
private final ValueEnvironment<UpperBounds> upperBounds;

/**
* Builds the pentagons.
*/
public Pentagons() {
this.intervals = new ValueEnvironment<>(new Interval()).top();
this.upperBounds = new ValueEnvironment<>(new UpperBounds(true)).top();
}

/**
* Builds the pentagons.
*
* @param intervals the underlying {@link ValueEnvironment<Interval>}
* @param upperBounds the underlying {@link ValueEnvironment<UpperBounds>}
*/
public Pentagons(ValueEnvironment<Interval> intervals, ValueEnvironment<UpperBounds> upperBounds) {
this.intervals = intervals;
this.upperBounds = upperBounds;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -25,23 +25,57 @@
import it.unive.lisa.util.representation.StringRepresentation;
import it.unive.lisa.util.representation.StructuredRepresentation;

/**
* The upper bounds abstract domain. It is implemented as
* a {@link BaseNonRelationalValueDomain}.
*
* @author <a href="mailto:[email protected]">Luca Negrini</a>
* @author <a href="mailto:[email protected]">Vincenzo Arceri</a>
*/
public class UpperBounds implements BaseNonRelationalValueDomain<UpperBounds>, Iterable<Identifier> {

/**
* The abstract top element.
*/
private static final UpperBounds TOP = new UpperBounds(true);

/**
* The abstract bottom element.
*/
private static final UpperBounds BOTTOM = new UpperBounds(new TreeSet<>());

/**
* The flag to set abstract top state.
*/
private final boolean isTop;

/**
* The set containing the bounds.
*/
private final Set<Identifier> bounds;

/**
* Builds the upper bounds.
*/
public UpperBounds() {
this(true);
}

/**
* Builds the upper bounds.
*
* @param isTop {@code true} if the abstract domain is top; otherwise {@code false}.
*/
public UpperBounds(boolean isTop) {
this.bounds = null;
this.isTop = isTop;
}

/**
* Builds the upper bounds.
*
* @param bounds the bounds to set
*/
public UpperBounds(Set<Identifier> bounds) {
this.bounds = bounds;
this.isTop = false;
Expand Down Expand Up @@ -168,10 +202,22 @@ public Iterator<Identifier> iterator() {
return bounds.iterator();
}

/**
* Checks if this bounds contains a specified identifier of a program variable.
*
* @param id the identifier to check
* @return {@code true} if this bounds contains the specified identifier; otherwise, {@code false}.
*/
public boolean contains(Identifier id) {
return bounds != null && bounds.contains(id);
}

/**
* Adds the specified identifier of a program variable in the bounds.
*
* @param id the identifier to add in the bounds.
* @return the updated bounds.
*/
public UpperBounds add(Identifier id) {
Set<Identifier> res = new HashSet<>();
if (!isTop() && !isBottom())
Expand Down

0 comments on commit ebda88b

Please sign in to comment.