This function symbol is created for casts to the depending sort.
An implicit restriction belongs to the arguments sorts. We will
forbid side casts from reference types to primtive types as this
usually indicates an error. But it should be stressed that the calculus
itself would remain sound even if we would syntactically allow such kind
of casts.
public CastFunctionSymbol(Sort argSort, Sort castSort)(Code)
creates an instance of a cast
Parameters: argSort - the Sort of the argument (usually any) Parameters: castSort - the Sort to be casted to
Method Detail
possibleSub
public boolean possibleSub(int at, Term possibleSub)(Code)
overrides method in
de.uka.ilkd.key.logic.op.Function and
inserts an additional check disallowing which disallows side casts
between primitive and reference types
Parameters: at - an int describing the planned sub term position of the given term Parameters: possibleSub - the Term designated to become the at-th sub term an boolean indicating if the given term is allowed at the given position