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.
|
Modifier and Type | Class and Description |
---|---|
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 |
PropositionalExpansionMacro
The macro PropositionalExpansionMacro apply rules to decompose propositional
toplevel formulas; but does not split the goal.
|
class |
PropositionalExpansionWithSimplificationMacro |
class |
UpdateSimplificationMacro
This macro applies only update simplification rules.
|
Copyright © 2003-2019 The KeY-Project.