All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type |
Method and Description |
private Quadruple<MethodFrame,ImmutableSet<LoopStatement>,ImmutableSet<StatementBlock>,ImmutableSet<MergePointStatement>> |
collectLoopsBlocksAndMergePointStatements(ProgramElement pe,
Services services) |
private Term |
determineSelfTerm(MethodFrame frame,
Services services) |
private Term |
initAtPreUpdate(java.lang.String methodName,
java.util.Map<LocationVariable,Term> atPres,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.Map<LocationVariable,LocationVariable> atPreHeapVars,
Services services,
TermBuilder tb) |
Term |
transform(Term term,
SVInstantiations svInst,
Services services)
initiates term transformation of term.
|
private Term |
updateAtPreUpdateForBlockAndLoopContracts(ImmutableSet<StatementBlock> blocks,
java.lang.String methodName,
java.util.Map<LocationVariable,Term> atPres,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.Map<LocationVariable,LocationVariable> atPreHeapVars,
Term atPreUpdate,
Services services,
TermBuilder tb) |
private Term |
updateAtPreUpdateForLoopInvariants(ImmutableSet<LoopStatement> loops,
java.lang.String methodName,
java.util.Map<LocationVariable,Term> atPres,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Term atPreUpdate,
Services services,
TermBuilder tb) |
private Term |
updateAtPreUpdateForMergePointStatements(ImmutableSet<MergePointStatement> mpss,
java.lang.String methodName,
java.util.Map<LocationVariable,Term> atPres,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Term atPreUpdate,
Services services,
TermBuilder tb) |
void |
updateBlockAndLoopContracts(ImmutableSet<? extends JavaStatement> statements,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.Map<LocationVariable,LocationVariable> atPreHeapVars,
Services services)
|
void |
updateBlockAndLoopContracts(ImmutableSet<StatementBlock> blocks,
ImmutableSet<LoopStatement> loops,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.Map<LocationVariable,LocationVariable> atPreHeapVars,
Services services)
|
private static void |
updateBlockOrLoopContract(JavaStatement statement,
AuxiliaryContract contract,
AuxiliaryContract.Variables newVariables,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
Services services) |
private Term |
updateLoopInvariants(ImmutableSet<LoopStatement> loops,
MethodFrame frame,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services,
TermBuilder tb) |
private void |
updateMergeContracts(ImmutableSet<MergePointStatement> mpss,
java.util.Map<LocationVariable,Term> atPres,
Services services) |