|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectescjava.translate.GetSpec
Responsible for getting Spec for calls. Includes ... from ESCJ16c.
Field Summary | |
private static java.util.HashSet |
collectInvariantsAxsToAdd
Collects the invariants in scope . |
private static ASTDecoration |
dmdDecoration
|
private static ASTDecoration |
nonnullDecoration
* Decorates GenericVarDecl 's to point to * NonNullPragmas
(SimpleModifierPragma's). |
Constructor Summary | |
GetSpec()
|
Method Summary | |
private static void |
addAssumptions(ExprVec ev,
StackVector code)
Appends code with an assume C command for
every condition C in cv . |
static void |
addAxioms(java.util.Set axsToAdd,
ExprVec assumptions)
axsToAdd holds a Set of RepHelper - we need to add to the assumptions any axioms pertinent to the RepHelper. |
static ConditionVec |
addConstraintClauses(ConditionVec post,
TypeDecl decl,
java.util.Hashtable wt,
ExprVec postAssumptions)
|
private static void |
addFreeTypeCorrectAs(GenericVarDecl vd,
Type type,
ConditionVec cv)
Adds to cv a condition stating that vd has
type type . |
private static void |
addInvariantBody(InvariantInfo ii,
Spec spec,
Set synTargs)
Extend spec , in a way appropriate for checking the body of
a method or constructor, to account for invariant ii.J
declared in class ii.U . |
private static void |
addModifiersToDMD(DerivedMethodDecl dmd,
RoutineDecl rd)
* Add the modifiers of rd to dmd, making any necessary substitions * of parameter names. |
private static ExprVec |
addNewAxs(java.util.HashSet axsToAdd,
ExprVec assumptions)
|
private static void |
addSuperInterfaces(TypeDecl td,
Set set)
|
private static void |
assumeConditions(ConditionVec cv,
StackVector code)
|
private static void |
checkConditions(ConditionVec cv,
int loc,
StackVector code)
Appends code with an check loc: C command for
every condition C in cv . |
private static void |
checkModifiesConstraints(Spec spec,
FindContributors scope,
Set syntargets,
java.util.Hashtable premap,
int loc,
StackVector code)
|
private static ExprVec |
collectAxioms(FindContributors scope)
Collects the axioms in scope . |
static void |
collectFields(Expr e,
java.util.Set s)
|
private static InvariantInfo |
collectInvariants(FindContributors scope,
java.util.Hashtable premap)
|
private static ParamAndGlobalVarInfo |
collectParamsAndGlobals(Spec spec,
FindContributors scope)
Collects the parameters of spec.args and the static fields
in scope , whose types are class types. |
(package private) static VariableAccess |
createVarVariant(GenericVarDecl vd,
java.lang.String postfix)
* Given a GenericVarDecl named "x@old", returns a VariableAccess to a * fresh LocalVarDecl named "x@ |
private static CondExprModifierPragma |
doSubst(java.util.Hashtable subst,
CondExprModifierPragma emp)
Perform a substitution on a CondExprModifierPragma * |
private static ExprModifierPragma |
doSubst(java.util.Hashtable subst,
ExprModifierPragma emp)
Perform a substitution on an ExprModifierPragma * |
private static VarExprModifierPragma |
doSubst(java.util.Hashtable subst,
VarExprModifierPragma vemp)
Perform a substitution on a VarExprModifierPragma * |
private static boolean |
exprIsVisible(TypeSig originType,
Expr e)
|
private static Spec |
extendSpecForBody(Spec spec,
FindContributors scope,
Set synTargs)
Implements ExtendSpecForBody, section 7.4 of ESCJ 16. |
private static Spec |
extendSpecForCall(Spec spec,
FindContributors scope,
Set predictedSynTargs)
Implements ExtendSpecForCall, section 7.3 of ESCJ 16. |
private static ExprModifierPragmaVec |
filterExprModPragmas(ExprModifierPragmaVec vec,
FindContributors scope)
|
static DerivedMethodDecl |
filterMethodDecl(DerivedMethodDecl dmd,
FindContributors scope)
|
private static ModifiesGroupPragmaVec |
filterModifies(ModifiesGroupPragmaVec mvec,
FindContributors scope)
|
private static VarExprModifierPragmaVec |
filterVarExprModPragmas(VarExprModifierPragmaVec vec,
FindContributors scope)
|
static DerivedMethodDecl |
getCombinedMethodDecl(RoutineDecl rd)
* Implement GetCombinedMethodDecl from ESCJ 16c section 7: * * Precondition: the type declaring rd has been typechecked. |
private static Spec |
getCommonSpec(RoutineDecl rd,
FindContributors scope,
java.util.Hashtable premap)
|
static java.util.Enumeration |
getFirstInheritedInterfaces(ClassDecl cd)
|
static TypeDeclElemVec |
getRepresentsClauses(TypeDecl td,
FieldDecl fd)
Gets the represents clauses for a model field fd as seen from a type declaration td; fd may be declared in td or in a supertype of td. |
static Spec |
getSpecForBody(RoutineDecl rd,
FindContributors scope,
Set synTargs,
java.util.Hashtable premap)
|
static Spec |
getSpecForCall(RoutineDecl rd,
FindContributors scope,
Set predictedSynTargs)
|
static Spec |
getSpecForInline(RoutineDecl rd,
FindContributors scope)
|
(package private) static java.util.Hashtable |
makeSubst(java.util.Enumeration e,
java.lang.String postfix)
Converts a GenericVarDecl enumeration to a mapping from those variables to new Variableaccesses. |
(package private) static java.util.Hashtable |
makeSubst(FormalParaDeclVec args,
java.lang.String postfix)
|
private static InvariantInfo |
mergeInvariants(InvariantInfo ii)
|
private static void |
nonNullInitChecks(TypeDecl td,
ConditionVec post)
Add to post all NonNullInit checks for non_null instance
fields and instance ghost fields declared in td . |
static SimpleModifierPragma |
NonNullPragma(GenericVarDecl v)
* Has a particular declaration been declared non_null? |
(package private) static java.util.Hashtable |
restrict(java.util.Hashtable map,
java.util.Enumeration e)
Creates and returns a new map that is map restricted to the
domain e . |
private static void |
setNonNullPragma(GenericVarDecl v,
SimpleModifierPragma nonnull)
* Mark v as non_null because of non_null pragma nonnull. * * Precondition: nonnull is a NON_NULL pragma. * * (Used to implement inheritence of non_null's.) |
private static VariableAccess |
shave(Expr e)
Shaves a GC designator. |
static SimpleModifierPragma |
superNonNullPragma(GenericVarDecl v)
Returns non-null if the formal parameter is declared non-null in some overridden declaration of the method. |
static GuardedCmd |
surroundBodyBySpec(GuardedCmd body,
Spec spec,
FindContributors scope,
Set syntargets,
java.util.Hashtable premap,
int locEndCurlyBrace)
Returns a command that first does an assume for each
precondition in spec , then does body , then
checks the postconditions of spec , and finally checks the
modifies constraints implied by spec . |
private static Spec |
trMethodDecl(DerivedMethodDecl dmd,
java.util.Hashtable premap)
Translates a MethodDecl to a Spec. |
private static ConditionVec |
trMethodDeclPostcondition(DerivedMethodDecl dmd,
java.util.Hashtable wt,
ExprVec postAssumptions)
Computes the postconditions, according to section 7.2.2 of ESCJ 16. |
private static ConditionVec |
trMethodDeclPreconditions(DerivedMethodDecl dmd,
ExprVec preAssumptions)
Computes the preconditions, according to section 7.2.0 of ESCJ 16. |
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
private static ASTDecoration dmdDecoration
private static java.util.HashSet collectInvariantsAxsToAdd
scope
.
private static ASTDecoration nonnullDecoration
GenericVarDecl
's to point to * NonNullPragmas
(SimpleModifierPragma's).
Constructor Detail |
public GetSpec()
Method Detail |
public static Spec getSpecForCall(RoutineDecl rd, FindContributors scope, Set predictedSynTargs)
public static Spec getSpecForInline(RoutineDecl rd, FindContributors scope)
public static Spec getSpecForBody(RoutineDecl rd, FindContributors scope, Set synTargs, java.util.Hashtable premap)
private static Spec getCommonSpec(RoutineDecl rd, FindContributors scope, java.util.Hashtable premap)
public static DerivedMethodDecl getCombinedMethodDecl(RoutineDecl rd)
* * Precondition: the type declaring rd has been typechecked.
* * Note: this routine may typecheck the supertypes of the type that * declares rd.
private static void addModifiersToDMD(DerivedMethodDecl dmd, RoutineDecl rd)
* * Precondition: rd has been typechecked.
private static ExprModifierPragma doSubst(java.util.Hashtable subst, ExprModifierPragma emp)
private static CondExprModifierPragma doSubst(java.util.Hashtable subst, CondExprModifierPragma emp)
private static VarExprModifierPragma doSubst(java.util.Hashtable subst, VarExprModifierPragma vemp)
public static DerivedMethodDecl filterMethodDecl(DerivedMethodDecl dmd, FindContributors scope)
private static ExprModifierPragmaVec filterExprModPragmas(ExprModifierPragmaVec vec, FindContributors scope)
private static ModifiesGroupPragmaVec filterModifies(ModifiesGroupPragmaVec mvec, FindContributors scope)
private static VarExprModifierPragmaVec filterVarExprModPragmas(VarExprModifierPragmaVec vec, FindContributors scope)
private static Spec trMethodDecl(DerivedMethodDecl dmd, java.util.Hashtable premap)
private static ConditionVec trMethodDeclPreconditions(DerivedMethodDecl dmd, ExprVec preAssumptions)
private static ConditionVec trMethodDeclPostcondition(DerivedMethodDecl dmd, java.util.Hashtable wt, ExprVec postAssumptions)
public static void addAxioms(java.util.Set axsToAdd, ExprVec assumptions)
public static ConditionVec addConstraintClauses(ConditionVec post, TypeDecl decl, java.util.Hashtable wt, ExprVec postAssumptions)
private static Spec extendSpecForCall(Spec spec, FindContributors scope, Set predictedSynTargs)
private static Spec extendSpecForBody(Spec spec, FindContributors scope, Set synTargs)
private static void nonNullInitChecks(TypeDecl td, ConditionVec post)
post
all NonNullInit checks for non_null instance
fields and instance ghost fields declared in td
.
public static java.util.Enumeration getFirstInheritedInterfaces(ClassDecl cd)
private static void addSuperInterfaces(TypeDecl td, Set set)
private static void addInvariantBody(InvariantInfo ii, Spec spec, Set synTargs)
spec
, in a way appropriate for checking the body of
a method or constructor, to account for invariant ii.J
declared in class ii.U
. The body to be checked has
syntactic targets synTargs
.
private static ExprVec collectAxioms(FindContributors scope)
scope
.
public static TypeDeclElemVec getRepresentsClauses(TypeDecl td, FieldDecl fd)
private static InvariantInfo collectInvariants(FindContributors scope, java.util.Hashtable premap)
private static ParamAndGlobalVarInfo collectParamsAndGlobals(Spec spec, FindContributors scope)
spec.args
and the static fields
in scope
, whose types are class types.
private static ExprVec addNewAxs(java.util.HashSet axsToAdd, ExprVec assumptions)
private static VariableAccess shave(Expr e)
static java.util.Hashtable restrict(java.util.Hashtable map, java.util.Enumeration e)
map
restricted to the
domain e
. Assumes that every element in e
is
in the domain of map
.
static java.util.Hashtable makeSubst(java.util.Enumeration e, java.lang.String postfix)
static java.util.Hashtable makeSubst(FormalParaDeclVec args, java.lang.String postfix)
static VariableAccess createVarVariant(GenericVarDecl vd, java.lang.String postfix)
private static void addFreeTypeCorrectAs(GenericVarDecl vd, Type type, ConditionVec cv)
cv
a condition stating that vd
has
type type
.
public static GuardedCmd surroundBodyBySpec(GuardedCmd body, Spec spec, FindContributors scope, Set syntargets, java.util.Hashtable premap, int locEndCurlyBrace)
assume
for each
precondition in spec
, then does body
, then
checks the postconditions of spec
, and finally checks the
modifies constraints implied by spec
.
private static void addAssumptions(ExprVec ev, StackVector code)
code
with an assume C
command for
every condition C
in cv
.
private static void assumeConditions(ConditionVec cv, StackVector code)
private static void checkConditions(ConditionVec cv, int loc, StackVector code)
code
with an check loc: C
command for
every condition C
in cv
.
private static void checkModifiesConstraints(Spec spec, FindContributors scope, Set syntargets, java.util.Hashtable premap, int loc, StackVector code)
private static InvariantInfo mergeInvariants(InvariantInfo ii)
private static boolean exprIsVisible(TypeSig originType, Expr e)
public static void collectFields(Expr e, java.util.Set s)
private static void setNonNullPragma(GenericVarDecl v, SimpleModifierPragma nonnull)
public static SimpleModifierPragma NonNullPragma(GenericVarDecl v)
* * Precondition: if the declaration is a formal parameter, then the * spec of it's routine has already been computed.
* * * WARNING: this is the only authorized way to determine this * information. Do *not* attempt to search for NON_NULL modifiers * directly. (This is needed to handle inherited NON_NULL's * properly.)
public static SimpleModifierPragma superNonNullPragma(GenericVarDecl v)
|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |