createExpressionSymbol(ProgramElementName p_name, KeYJavaType p_type, ListOfIProgramVariable p_influencingPVs, ArrayOfStatement p_jumpTable) Create a skolem symbol for expressions
Parameters: p_name - name of the symbol Parameters: p_type - result type the symbol shall have Parameters: p_influencingPVs - program variable arguments the symbol is tobe given.
Constructor Detail
ExpressionSkolemSymbolFactory
public ExpressionSkolemSymbolFactory(Services p_services)(Code)
Create a skolem symbol for expressions
Parameters: p_name - name of the symbol Parameters: p_type - result type the symbol shall have Parameters: p_influencingPVs - program variable arguments the symbol is tobe given. A result variable of type p_type and a selector variable of type int are added as the last two argumentsimplicitly Parameters: jumpTable - the jump table that symbol should have
Methods inherited from de.uka.ilkd.key.rule.soundness.SkolemSymbolTacletFactory