Package | Description |
---|---|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
Modifier and Type | Method and Description |
---|---|
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) |
Modifier and Type | Method and Description |
---|---|
protected void |
AbstractBlockContractRule.setUpInfFlowPartOfUsageGoal(Goal usageGoal,
AbstractBlockContractRule.InfFlowValidityData infFlowValitidyData,
Term contextUpdate,
Term remembranceUpdate,
Term anonymisationUpdate,
TermBuilder tb) |
Copyright © 2003-2019 The KeY-Project.