static ImmutableSet<BlockContract> |
AbstractBlockContractRule.getApplicableContracts(AbstractAuxiliaryContractRule.Instantiation instantiation,
Goal goal,
Services services) |
static ImmutableSet<LoopContract> |
AbstractLoopContractRule.getApplicableContracts(AbstractAuxiliaryContractRule.Instantiation instantiation,
Goal goal,
Services services) |
protected void |
BlockContractExternalRule.setLastInstantiation(AbstractAuxiliaryContractRule.Instantiation lastInstantiation) |
protected void |
BlockContractInternalRule.setLastInstantiation(AbstractAuxiliaryContractRule.Instantiation lastInstantiation) |
protected void |
LoopContractExternalRule.setLastInstantiation(AbstractAuxiliaryContractRule.Instantiation lastInstantiation) |
protected abstract void |
AbstractAuxiliaryContractRule.setLastInstantiation(AbstractAuxiliaryContractRule.Instantiation inst) |
protected void |
LoopContractInternalRule.setLastInstantiation(AbstractAuxiliaryContractRule.Instantiation lastInstantiation) |
protected AbstractBlockContractRule.InfFlowValidityData |
AbstractBlockContractRule.setUpInfFlowValidityGoal(Goal infFlowGoal,
BlockContract contract,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
Services services,
AuxiliaryContract.Variables variables,
ProgramVariable exceptionParameter,
java.util.List<LocationVariable> heaps,
ImmutableSet<ProgramVariable> localInVariables,
ImmutableSet<ProgramVariable> localOutVariables,
BlockContractInternalBuiltInRuleApp application,
AbstractAuxiliaryContractRule.Instantiation instantiation) |