gov.llnl.babel.symbols

Class Assertion


public class Assertion
extends ASTNode

Field Summary

static int
ENSURE
static int
ENSURE_THEN
static int
INVARIANT
static int
REQUIRE
static int
REQUIRE_ELSE
static int
UNKNOWN
static String[]
s_names

Fields inherited from class gov.llnl.babel.symbols.ASTNode

d_frozen

Constructor Summary

Assertion(int type, String source, String tag, Comment comment)
Create a new object.

Method Summary

String
cExpression(String epvVar, int[] startInd)
Return the C version of the expression used to check for violation.
protected void
ensureNoPostAssertions(AssertionExpression expr)
Ensure the expression does not contain any (sub)expressions specifically for post-condition assertions.
String
errorMessage()
Return the error message associated with a failure of this assertion.
void
freeze()
ArrayList
getArrayIterMacros(String epvVar, int[] startInd)
Return the list of array iteration macro messages, if any.
Comment
getComment()
Return the comment, if any, associated with this list of object states.
protected String
getExceptionPrefix(Extendable ext, Method m)
Return the prefix for exception messages based on the specified extendable and method.
AssertionExpression
getExpression()
Return the assertion expression.
int
getNumArrayIterMacrosByType(char type)
Returns the number of macros supported by this assertion of the specified type.
String
getSource()
Return the source associated with this assertion.
String
getTag()
Return the tag associated with this list of object states.
int
getType()
Return the type of the assertion.
int
getType(String name)
Return the type of the assertion specified by name.
String
getTypeName()
Return the name of the type of the assertion.
boolean
hasMethodCall()
Return TRUE if a method call is found within the expression; otherwise, return FALSE.
boolean
hasPureClause()
Return TRUE if a pure clause is found within the expression; otherwise, return FALSE.
boolean
hasReservedMethod(int type)
Return TRUE if the specified reserved method call is found within the expression; otherwise, return FALSE.
boolean
hasResult()
Return TRUE if a result clause is found within the expression; otherwise, return FALSE.
boolean
hasUnreservedMethod(boolean any)
Return TRUE if the method is any unreserved method (when any is TRUE) or it is an unreserved method with a throws clause (if any is FALSE); otherwise, return FALSE.
boolean
isInvariant()
Return TRUE if an invariant; otherwise, returns FALSE.
boolean
isPostcondition()
Return TRUE if a postcondition; otherwise, returns FALSE.
boolean
isPrecondition()
Return TRUE if a precondition; otherwise, returns FALSE.
boolean
isValid()
Return TRUE if the expression has been validated; otherwise, return FALSE.
void
setExpression(AssertionExpression expr)
Set the assertion expression.
String
toString()
Return the stringified version of the expression (in SIDL form) BUT without the comment.
void
validateExpression(Extendable ext, Method m, boolean skip)
Validate the assertion expression within the context of the given extendable and optional method.

Methods inherited from class gov.llnl.babel.symbols.ASTNode

checkFrozen, clone, freeze, protectCollection, protectList, protectMap, protectSet

Field Details

ENSURE

public static final int ENSURE
Field Value:
4

ENSURE_THEN

public static final int ENSURE_THEN
Field Value:
5

INVARIANT

public static final int INVARIANT
Field Value:
1

REQUIRE

public static final int REQUIRE
Field Value:
2

REQUIRE_ELSE

public static final int REQUIRE_ELSE
Field Value:
3

UNKNOWN

public static final int UNKNOWN
Field Value:
0

s_names

public static final String[] s_names

Constructor Details

Assertion

public Assertion(int type,
                 String source,
                 String tag,
                 Comment comment)
            throws AssertionException
Create a new object.
Parameters:
type - The type of the assertion.
source - The owning interface or class. For use in generated debug messages.
tag - The tag, if any, associated with the assertion. For use in generated debug messags.
comment - The comment, if any, associated with the assertion.
Throws:
AssertionException - The exception raised if assertion type is invalid.

Method Details

cExpression

public String cExpression(String epvVar,
                          int[] startInd)
Return the C version of the expression used to check for violation.

ensureNoPostAssertions

protected void ensureNoPostAssertions(AssertionExpression expr)
            throws AssertionException
Ensure the expression does not contain any (sub)expressions specifically for post-condition assertions. For example, the assertion should not contain a PURE or RESULT clause.
Parameters:
expr - The assertion expression being checked.
Throws:
AssertionException - The exception raised if post-condition assertions present.

errorMessage

public String errorMessage()
Return the error message associated with a failure of this assertion.

freeze

public void freeze()
Overrides:
freeze in interface ASTNode

getArrayIterMacros

public ArrayList getArrayIterMacros(String epvVar,
                                    int[] startInd)
Return the list of array iteration macro messages, if any. Each message is a string where the first character indicates the return type associated with the iteration. The remaining characters will be the actual macro invocation.

getComment

public Comment getComment()
Return the comment, if any, associated with this list of object states.

getExceptionPrefix

protected String getExceptionPrefix(Extendable ext,
                                    Method m)
Return the prefix for exception messages based on the specified extendable and method.
Parameters:
ext - The interface or class that owns this expression.
m - The method that owns this expression.

getExpression

public AssertionExpression getExpression()
Return the assertion expression.

getNumArrayIterMacrosByType

public int getNumArrayIterMacrosByType(char type)
Returns the number of macros supported by this assertion of the specified type. Valid types are given in MethodCall.java.

getSource

public String getSource()
Return the source associated with this assertion.

getTag

public String getTag()
Return the tag associated with this list of object states.

getType

public int getType()
Return the type of the assertion.

getType

public int getType(String name)
Return the type of the assertion specified by name.
Parameters:
name - The name of the type of assertion whose type is to be returned.

getTypeName

public String getTypeName()
Return the name of the type of the assertion. It is assumed the type is valid/known thanks to the check in the constructor.

hasMethodCall

public boolean hasMethodCall()
Return TRUE if a method call is found within the expression; otherwise, return FALSE.

hasPureClause

public boolean hasPureClause()
Return TRUE if a pure clause is found within the expression; otherwise, return FALSE.

hasReservedMethod

public boolean hasReservedMethod(int type)
Return TRUE if the specified reserved method call is found within the expression; otherwise, return FALSE.

hasResult

public boolean hasResult()
Return TRUE if a result clause is found within the expression; otherwise, return FALSE.

hasUnreservedMethod

public boolean hasUnreservedMethod(boolean any)
Return TRUE if the method is any unreserved method (when any is TRUE) or it is an unreserved method with a throws clause (if any is FALSE); otherwise, return FALSE.

isInvariant

public boolean isInvariant()
Return TRUE if an invariant; otherwise, returns FALSE.

isPostcondition

public boolean isPostcondition()
Return TRUE if a postcondition; otherwise, returns FALSE.

isPrecondition

public boolean isPrecondition()
Return TRUE if a precondition; otherwise, returns FALSE.

isValid

public boolean isValid()
Return TRUE if the expression has been validated; otherwise, return FALSE.

setExpression

public void setExpression(AssertionExpression expr)
            throws AssertionException
Set the assertion expression. Note this is added during syntactic parsing so not all of the information for evaluating the validity of the expression is available (e.g., function return values). Hence, the validity of the expression itself is left as a separate step in the process once the symbols for the associated extendable are created. Assumptions: 1) requiresMethodContext() returns TRUE ONLY if the assertion expression really requires method context. For example, an expression that contains a method call with no arguments only requires the extendable context, NOT the method context. Same is TRUE if the arguments are literals. However, method context is required if one or more of the arguments are identifiers.
Parameters:
expr - The assertion expression being checked.
Throws:
AssertionException - The exception raised if type validation fails.

toString

public String toString()
Return the stringified version of the expression (in SIDL form) BUT without the comment. That must be retrieved separately.

validateExpression

public void validateExpression(Extendable ext,
                               Method m,
                               boolean skip)
            throws AssertionException
Validate the assertion expression within the context of the given extendable and optional method.
Parameters:
ext - The interface or class that owns this expression.
m - The method that owns this expression.
skip - If TRUE, will skip the validation process if the expression has already been marked as being valid.
Throws:
AssertionException - The exception that can be raised during the validation.