|
| |
|
| java.lang.Object
 de.uka.ilkd.key.logic.op.Op
de.uka.ilkd.key.logic.op.AbstractMetaOperator
de.uka.ilkd.key.rule.metaconstruct.ArrayStoreStaticAnalyse
| ArrayStoreStaticAnalyse | | public class ArrayStoreStaticAnalyse extends AbstractMetaOperator (Code) | | This metaconstruct tries to statically determine whether an array component
assignment is safe, i.e. does not lead to an ArrayStoreException
Currently it makes use of a strong closed world assumption which could be relaxed
(of course by loss of power) to a version wo closed world asssumptions making
use of the final modifier of classes.
TODO: add features for multi-dimensional arrays
|
| ArrayStoreStaticAnalyse | | public ArrayStoreStaticAnalyse()(Code) | | creates this metaconstruct
|
| calculate | | public Term calculate(Term term, SVInstantiations svInst, Services services)(Code) | | tries to determine whether the predicate "arrayStoreValid" is true or
false using type analysis. It makes some strong closed world assumptions.
A weaker version without closed world assumption is possible making use of
the final modifier of classes.
It assumes that teh first argumnet of arrayStoreValid is not
equal to null
|
|
|
|