Skip to content

Commit

Permalink
Fixing javadoc visibility problems
Browse files Browse the repository at this point in the history
  • Loading branch information
lucaneg committed Sep 14, 2023
1 parent 7e77c69 commit 1e73fab
Show file tree
Hide file tree
Showing 13 changed files with 69 additions and 82 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -209,18 +209,16 @@ protected C extrapolationHeuristic(C other) throws SemanticException {
* Given two subset S<sub>1</sub> and S<sub>2</sub> of the domain of a
* lattice widening(S<sub>1</sub>, S<sub>2</sub>) =
* h<sup>&nabla;</sup>(S<sub>1</sub>, T<sub>2</sub>), where
* h<sup>&nabla;</sup> is a
* {@link #extrapolationHeuristic(NonRedundantPowerset) widenining-connected
* extrapolation heuristic} and T<sub>2</sub> is equal to:
* h<sup>&nabla;</sup> is a widenining-connected extrapolation heuristic and
* T<sub>2</sub> is equal to:
* <ul>
* <li>S<sub>2</sub> &ensp;&ensp;&ensp;&ensp;&ensp;&ensp;&ensp; if
* S<sub>1</sub> &le;<sub>EM</sub> S<sub>2</sub></li>
* <li>S<sub>1</sub> +<sub>EM</sub> S<sub>2</sub> &ensp; otherwise</li>
* </ul>
* where &le;<sub>EM</sub> is the
* {@link #lessOrEqualEgliMilner(NonRedundantPowerset) Egli-Milner relation}
* and +<sub>EM</sub> is an
* {@link #EgliMilnerConnector(NonRedundantPowerset) Egli-Milner connector}.
* and +<sub>EM</sub> is an Egli-Milner connector.
*/
@Override
public C wideningAux(C other) throws SemanticException {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -297,20 +297,16 @@ protected C extrapolationHeuristic(C other) throws SemanticException {
* Given two subset S<sub>1</sub> and S<sub>2</sub> of the domain of a
* lattice widening(S<sub>1</sub>, S<sub>2</sub>) =
* h<sup>&nabla;</sup>(S<sub>1</sub>, T<sub>2</sub>), where
* h<sup>&nabla;</sup> is a
* {@link #extrapolationHeuristic(NonRedundantPowersetOfBaseNonRelationalValueDomain)
* widenining-connected extrapolation heuristic} and T<sub>2</sub> is equal
* to:
* h<sup>&nabla;</sup> is a widenining-connected extrapolation heuristic and
* T<sub>2</sub> is equal to:
* <ul>
* <li>S<sub>2</sub> &ensp;&ensp;&ensp;&ensp;&ensp;&ensp;&ensp; if
* S<sub>1</sub> &le;<sub>EM</sub> S<sub>2</sub></li>
* <li>S<sub>1</sub> +<sub>EM</sub> S<sub>2</sub> &ensp; otherwise</li>
* </ul>
* where &le;<sub>EM</sub> is the
* {@link #lessOrEqualEgliMilner(NonRedundantPowersetOfBaseNonRelationalValueDomain)
* Egli-Milner relation} and +<sub>EM</sub> is an
* {@link #EgliMilnerConnector(NonRedundantPowersetOfBaseNonRelationalValueDomain)
* Egli-Milner connector}.
* Egli-Milner relation} and +<sub>EM</sub> is an Egli-Milner connector.
*/
@Override
public C wideningAux(C other) throws SemanticException {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -25,13 +25,12 @@
* {@link StringType}. <br>
* <br>
* Since in most languages string operations are provided through calls to
* library functions, this class contains a field {@link #originating} whose
* purpose is to optionally store a {@link Statement} that is rewritten to an
* instance of this class (i.e., a call to a {@link NativeCFG} modeling the
* library function). If present, such statement will be used as
* {@link ProgramPoint} for semantics computations. This allows subclasses to
* implement {@link PluggableStatement} easily without redefining the semantics
* provided by this class.
* library functions, this class contains a field whose purpose is to optionally
* store a {@link Statement} that is rewritten to an instance of this class
* (i.e., a call to a {@link NativeCFG} modeling the library function). If
* present, such statement will be used as {@link ProgramPoint} for semantics
* computations. This allows subclasses to implement {@link PluggableStatement}
* easily without redefining the semantics provided by this class.
*
* @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
*/
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -26,13 +26,12 @@
* {@link BooleanType}. <br>
* <br>
* Since in most languages string operations are provided through calls to
* library functions, this class contains a field {@link #originating} whose
* purpose is to optionally store a {@link Statement} that is rewritten to an
* instance of this class (i.e., a call to a {@link NativeCFG} modeling the
* library function). If present, such statement will be used as
* {@link ProgramPoint} for semantics computations. This allows subclasses to
* implement {@link PluggableStatement} easily without redefining the semantics
* provided by this class.
* library functions, this class contains a field whose purpose is to optionally
* store a {@link Statement} that is rewritten to an instance of this class
* (i.e., a call to a {@link NativeCFG} modeling the library function). If
* present, such statement will be used as {@link ProgramPoint} for semantics
* computations. This allows subclasses to implement {@link PluggableStatement}
* easily without redefining the semantics provided by this class.
*
* @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
*/
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -26,13 +26,12 @@
* {@link BooleanType}. <br>
* <br>
* Since in most languages string operations are provided through calls to
* library functions, this class contains a field {@link #originating} whose
* purpose is to optionally store a {@link Statement} that is rewritten to an
* instance of this class (i.e., a call to a {@link NativeCFG} modeling the
* library function). If present, such statement will be used as
* {@link ProgramPoint} for semantics computations. This allows subclasses to
* implement {@link PluggableStatement} easily without redefining the semantics
* provided by this class.
* library functions, this class contains a field whose purpose is to optionally
* store a {@link Statement} that is rewritten to an instance of this class
* (i.e., a call to a {@link NativeCFG} modeling the library function). If
* present, such statement will be used as {@link ProgramPoint} for semantics
* computations. This allows subclasses to implement {@link PluggableStatement}
* easily without redefining the semantics provided by this class.
*
* @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
*/
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -26,13 +26,12 @@
* {@link BooleanType}. <br>
* <br>
* Since in most languages string operations are provided through calls to
* library functions, this class contains a field {@link #originating} whose
* purpose is to optionally store a {@link Statement} that is rewritten to an
* instance of this class (i.e., a call to a {@link NativeCFG} modeling the
* library function). If present, such statement will be used as
* {@link ProgramPoint} for semantics computations. This allows subclasses to
* implement {@link PluggableStatement} easily without redefining the semantics
* provided by this class.
* library functions, this class contains a field whose purpose is to optionally
* store a {@link Statement} that is rewritten to an instance of this class
* (i.e., a call to a {@link NativeCFG} modeling the library function). If
* present, such statement will be used as {@link ProgramPoint} for semantics
* computations. This allows subclasses to implement {@link PluggableStatement}
* easily without redefining the semantics provided by this class.
*
* @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
*/
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -26,13 +26,12 @@
* {@link NumericType}. <br>
* <br>
* Since in most languages string operations are provided through calls to
* library functions, this class contains a field {@link #originating} whose
* purpose is to optionally store a {@link Statement} that is rewritten to an
* instance of this class (i.e., a call to a {@link NativeCFG} modeling the
* library function). If present, such statement will be used as
* {@link ProgramPoint} for semantics computations. This allows subclasses to
* implement {@link PluggableStatement} easily without redefining the semantics
* provided by this class.
* library functions, this class contains a field whose purpose is to optionally
* store a {@link Statement} that is rewritten to an instance of this class
* (i.e., a call to a {@link NativeCFG} modeling the library function). If
* present, such statement will be used as {@link ProgramPoint} for semantics
* computations. This allows subclasses to implement {@link PluggableStatement}
* easily without redefining the semantics provided by this class.
*
* @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
*/
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -26,13 +26,12 @@
* {@link NumericType}. <br>
* <br>
* Since in most languages string operations are provided through calls to
* library functions, this class contains a field {@link #originating} whose
* purpose is to optionally store a {@link Statement} that is rewritten to an
* instance of this class (i.e., a call to a {@link NativeCFG} modeling the
* library function). If present, such statement will be used as
* {@link ProgramPoint} for semantics computations. This allows subclasses to
* implement {@link PluggableStatement} easily without redefining the semantics
* provided by this class.
* library functions, this class contains a field whose purpose is to optionally
* store a {@link Statement} that is rewritten to an instance of this class
* (i.e., a call to a {@link NativeCFG} modeling the library function). If
* present, such statement will be used as {@link ProgramPoint} for semantics
* computations. This allows subclasses to implement {@link PluggableStatement}
* easily without redefining the semantics provided by this class.
*
* @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
*/
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -25,13 +25,12 @@
* {@link StringType}. <br>
* <br>
* Since in most languages string operations are provided through calls to
* library functions, this class contains a field {@link #originating} whose
* purpose is to optionally store a {@link Statement} that is rewritten to an
* instance of this class (i.e., a call to a {@link NativeCFG} modeling the
* library function). If present, such statement will be used as
* {@link ProgramPoint} for semantics computations. This allows subclasses to
* implement {@link PluggableStatement} easily without redefining the semantics
* provided by this class.
* library functions, this class contains a field whose purpose is to optionally
* store a {@link Statement} that is rewritten to an instance of this class
* (i.e., a call to a {@link NativeCFG} modeling the library function). If
* present, such statement will be used as {@link ProgramPoint} for semantics
* computations. This allows subclasses to implement {@link PluggableStatement}
* easily without redefining the semantics provided by this class.
*
* @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
*/
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -26,13 +26,12 @@
* {@link BooleanType}. <br>
* <br>
* Since in most languages string operations are provided through calls to
* library functions, this class contains a field {@link #originating} whose
* purpose is to optionally store a {@link Statement} that is rewritten to an
* instance of this class (i.e., a call to a {@link NativeCFG} modeling the
* library function). If present, such statement will be used as
* {@link ProgramPoint} for semantics computations. This allows subclasses to
* implement {@link PluggableStatement} easily without redefining the semantics
* provided by this class.
* library functions, this class contains a field whose purpose is to optionally
* store a {@link Statement} that is rewritten to an instance of this class
* (i.e., a call to a {@link NativeCFG} modeling the library function). If
* present, such statement will be used as {@link ProgramPoint} for semantics
* computations. This allows subclasses to implement {@link PluggableStatement}
* easily without redefining the semantics provided by this class.
*
* @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
*/
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -27,13 +27,12 @@
* {@link StringType}. <br>
* <br>
* Since in most languages string operations are provided through calls to
* library functions, this class contains a field {@link #originating} whose
* purpose is to optionally store a {@link Statement} that is rewritten to an
* instance of this class (i.e., a call to a {@link NativeCFG} modeling the
* library function). If present, such statement will be used as
* {@link ProgramPoint} for semantics computations. This allows subclasses to
* implement {@link PluggableStatement} easily without redefining the semantics
* provided by this class.
* library functions, this class contains a field whose purpose is to optionally
* store a {@link Statement} that is rewritten to an instance of this class
* (i.e., a call to a {@link NativeCFG} modeling the library function). If
* present, such statement will be used as {@link ProgramPoint} for semantics
* computations. This allows subclasses to implement {@link PluggableStatement}
* easily without redefining the semantics provided by this class.
*
* @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
*/
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -23,10 +23,11 @@

/**
* A fixpoint algorithm for a {@link Graph}, parametric to the
* {@link FixpointImplementation} that one wants to use to compute the results.
* This fixpoint algorithms is optimized: it works exploiting the basic blocks
* of the target graph, and only yields approximations of widening points,
* stopping statements and user-defined hotspots.
* {@link it.unive.lisa.util.datastructures.graph.algorithms.Fixpoint.FixpointImplementation}
* that one wants to use to compute the results. This fixpoint algorithms is
* optimized: it works exploiting the basic blocks of the target graph, and only
* yields approximations of widening points, stopping statements and
* user-defined hotspots.
*
* @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
*
Expand Down
Original file line number Diff line number Diff line change
@@ -1,18 +1,19 @@
package it.unive.lisa.symbolic.value.operator.binary;

import java.util.Collections;
import java.util.Set;

import it.unive.lisa.symbolic.value.operator.StringOperator;
import it.unive.lisa.type.StringType;
import it.unive.lisa.type.Type;
import it.unive.lisa.type.TypeSystem;
import java.util.Collections;
import java.util.Set;

/**
* A common implementation for classes implementing {@link BinaryOperator} and
* {@link StringOperator}, providing a
* {@link #typeInference(TypeSystem, Set, Set)} implementation that returns an
* empty set if no {@link StringType} can be found in one of the arguments, and
* a singleton set containing {@link #resultType(TypeSystem)} otherwise.
* a singleton set containing their result type otherwise.
*
* @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
*/
Expand Down

0 comments on commit 1e73fab

Please sign in to comment.