Package | Description |
---|---|
de.uka.ilkd.key.informationflow.macros | |
de.uka.ilkd.key.macros |
Modifier and Type | Class and Description |
---|---|
class |
SelfcompositionStateExpansionMacro
The macro SelfcompositionStateExpansionMacro applies rules to extract
the self-composed states after the merge of the symbolic execution goals
which is included in the proof obligation generation from information flow
contracts.
|
class |
UseInformationFlowContractMacro
The macro UseInformationFlowContractMacro applies all applicable information
flow contracts.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractBlastingMacro |
class |
AbstractPropositionalExpansionMacro
The Class AbstractPropositionalExpansionMacro applies purely propositional
rules.
|
class |
AutoMacro
The macro
AutoMacro is a customizable ProofMacro for use in
proof scripts. |
class |
AutoPilotPrepareProofMacro |
class |
FinishSymbolicExecutionMacro
The macro FinishSymbolicExecutionMacro continues automatic rule application
until there is no more modality on the sequent.
|
class |
FinishSymbolicExecutionUntilMergePointMacro
The macro FinishSymbolicExecutionUntilJionPointMacro continues automatic rule
application until a merge point is reached (i.e.
|
class |
FullPropositionalExpansionMacro
The macro FullPropositionalExpansionMacro apply rules to decompose
propositional toplevel formulas; it even splits the goal if necessary.
|
class |
HeapSimplificationMacro
This macro performs simplification of Heap and LocSet terms.
|
class |
IntegerSimplificationMacro
This macro performs simplification of integers and terms with integers.
|
class |
OneStepProofMacro
Apply a single proof step.
|
class |
PrepareInfFlowContractPreBranchesMacro
The macro UseInformationFlowContractMacro applies all applicable information
flow contracts.
|
class |
PropositionalExpansionMacro
The macro PropositionalExpansionMacro apply rules to decompose propositional
toplevel formulas; but does not split the goal.
|
class |
PropositionalExpansionWithSimplificationMacro |
class |
SemanticsBlastingMacro |
class |
TestGenMacro |
class |
UpdateSimplificationMacro
This macro applies only update simplification rules.
|
class |
WellDefinednessMacro
This macro resolves the well-definedness transformer, i.e.
|
Copyright © 2003-2019 The KeY-Project.