fmrisc.ProgramExplorer.Semantics

Class TypeTranslator

java.lang.Object

fmrisc.ProgramExplorer.Semantics.TypeTranslator

public class TypeTranslator
extends java.lang.Object

Translate program types to logical types.

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	arrayLength
static java.lang.String	arrayValue
static java.lang.String	baseTheoryName
static java.lang.String	charName
static java.lang.String	intDivName
static java.lang.String	intDivName0
static java.lang.String	intDivOverflowName
static java.lang.String	intMinusName
static java.lang.String	intMinusOverflowName
static java.lang.String	intName
static java.lang.String	intNegName
static java.lang.String	intNegOverflowName
static java.lang.String	intPlusName
static java.lang.String	intPlusOverflowName
static java.lang.String	intRemName
static java.lang.String	intTimesName
static java.lang.String	intTimesOverflowName
static java.lang.String	intTruncName
static java.lang.String	isNullName
static java.lang.String	maxIntName
static java.lang.String	minIntName
static java.lang.String	natName
static java.lang.String	newArrayAxiomName
static java.lang.String	newArrayName
static java.lang.String	newBooleanArrayAxiomName
static java.lang.String	newBooleanArrayName
static java.lang.String	newCharArrayAxiomName
static java.lang.String	newCharArrayName
static java.lang.String	newIntArrayAxiomName
static java.lang.String	newIntArrayName
static java.lang.String	newName
static java.lang.String	newObjectName
static java.lang.String	newStringArrayAxiomName
static java.lang.String	newStringArrayName
static java.lang.String	newStringName
static java.lang.String	nullArrayName
static java.lang.String	nullBooleanArrayName
static java.lang.String	nullCharArrayName
static java.lang.String	nullCharName
static java.lang.String	nullIntArrayName
static java.lang.String	nullName
static java.lang.String	nullStringArrayName
static java.lang.String	nullStringName
static java.lang.String	typeArrayName
static java.lang.String	typeBooleanArrayName
static java.lang.String	typeCharArrayName
static java.lang.String	typeIntArrayName
static java.lang.String	typeStringArrayName
static java.lang.String	zeroName

Constructor Summary

Constructors

Constructor and Description
TypeTranslator() Construct type translator for given root package.

Method Summary

Modifier and Type	Method and Description
TheoryDeclaration	constructClassTheory(ClassSymbol csymbol) Construct a theory declaration for the denoted class.
TheorySymbol	getBaseTheory() Get the base theory symbol.
TheorySymbol	getStringTheory() Get the current string theory
Type	getStringType() Get the current string type.
void	init(PackageSymbol top, ErrorStream error) Initialize type translator (which creates a base theory).
Type	logicType(TypeExpression exp) Translate a program's type expression to a logical type.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

baseTheoryName

public static final java.lang.String baseTheoryName

See Also:

Constant Field Values

minIntName

public static final java.lang.String minIntName

See Also:

Constant Field Values

maxIntName

public static final java.lang.String maxIntName

See Also:

Constant Field Values

intName

public static final java.lang.String intName

See Also:

Constant Field Values

natName

public static final java.lang.String natName

See Also:

Constant Field Values

charName

public static final java.lang.String charName

See Also:

Constant Field Values

intPlusName

public static final java.lang.String intPlusName

See Also:

Constant Field Values

intNegName

public static final java.lang.String intNegName

See Also:

Constant Field Values

intMinusName

public static final java.lang.String intMinusName

See Also:

Constant Field Values

intTimesName

public static final java.lang.String intTimesName

See Also:

Constant Field Values

intDivName

public static final java.lang.String intDivName

See Also:

Constant Field Values

intDivName0

public static final java.lang.String intDivName0

See Also:

Constant Field Values

intRemName

public static final java.lang.String intRemName

See Also:

Constant Field Values

intPlusOverflowName

public static final java.lang.String intPlusOverflowName

See Also:

Constant Field Values

intNegOverflowName

public static final java.lang.String intNegOverflowName

See Also:

Constant Field Values

intMinusOverflowName

public static final java.lang.String intMinusOverflowName

See Also:

Constant Field Values

intTimesOverflowName

public static final java.lang.String intTimesOverflowName

See Also:

Constant Field Values

intTruncName

public static final java.lang.String intTruncName

See Also:

Constant Field Values

intDivOverflowName

public static final java.lang.String intDivOverflowName

See Also:

Constant Field Values

zeroName

public static final java.lang.String zeroName

See Also:

Constant Field Values

nullCharName

public static final java.lang.String nullCharName

See Also:

Constant Field Values

nullStringName

public static final java.lang.String nullStringName

See Also:

Constant Field Values

newStringName

public static final java.lang.String newStringName

See Also:

Constant Field Values

typeIntArrayName

public static final java.lang.String typeIntArrayName

See Also:

Constant Field Values

typeCharArrayName

public static final java.lang.String typeCharArrayName

See Also:

Constant Field Values

typeBooleanArrayName

public static final java.lang.String typeBooleanArrayName

See Also:

Constant Field Values

typeStringArrayName

public static final java.lang.String typeStringArrayName

See Also:

Constant Field Values

nullIntArrayName

public static final java.lang.String nullIntArrayName

See Also:

Constant Field Values

nullCharArrayName

public static final java.lang.String nullCharArrayName

See Also:

Constant Field Values

nullBooleanArrayName

public static final java.lang.String nullBooleanArrayName

See Also:

Constant Field Values

nullStringArrayName

public static final java.lang.String nullStringArrayName

See Also:

Constant Field Values

newIntArrayName

public static final java.lang.String newIntArrayName

See Also:

Constant Field Values

newCharArrayName

public static final java.lang.String newCharArrayName

See Also:

Constant Field Values

newBooleanArrayName

public static final java.lang.String newBooleanArrayName

See Also:

Constant Field Values

newStringArrayName

public static final java.lang.String newStringArrayName

See Also:

Constant Field Values

newIntArrayAxiomName

public static final java.lang.String newIntArrayAxiomName

See Also:

Constant Field Values

newCharArrayAxiomName

public static final java.lang.String newCharArrayAxiomName

See Also:

Constant Field Values

newBooleanArrayAxiomName

public static final java.lang.String newBooleanArrayAxiomName

See Also:

Constant Field Values

newStringArrayAxiomName

public static final java.lang.String newStringArrayAxiomName

See Also:

Constant Field Values

typeArrayName

public static final java.lang.String typeArrayName

See Also:

Constant Field Values

nullName

public static final java.lang.String nullName

See Also:

Constant Field Values

newObjectName

public static final java.lang.String newObjectName

See Also:

Constant Field Values

nullArrayName

public static final java.lang.String nullArrayName

See Also:

Constant Field Values

newArrayName

public static final java.lang.String newArrayName

See Also:

Constant Field Values

newArrayAxiomName

public static final java.lang.String newArrayAxiomName

See Also:

Constant Field Values

arrayLength

public static final java.lang.String arrayLength

See Also:

Constant Field Values

arrayValue

public static final java.lang.String arrayValue

See Also:

Constant Field Values

isNullName

public static final java.lang.String isNullName

See Also:

Constant Field Values

newName

public static final java.lang.String newName

See Also:

Constant Field Values

Constructor Detail

TypeTranslator

public TypeTranslator()

Construct type translator for given root package. Still need to be initialized.

Method Detail

getStringType

public Type getStringType()

Get the current string type.

Returns:

the string type.

getStringTheory

public TheorySymbol getStringTheory()

Get the current string theory

Returns:

the string theory.

init

public void init(PackageSymbol top,
                 ErrorStream error)

Initialize type translator (which creates a base theory).

Parameters:

top - the root package to be used for initialization.

error - the error stream.

getBaseTheory

public TheorySymbol getBaseTheory()

Get the base theory symbol.

Returns:

the symbol of the base theory.

logicType

public Type logicType(TypeExpression exp)

Translate a program's type expression to a logical type.

Parameters:

exp - a type expression that does not contain the "void" type

Returns:

the logical type (null, if something went wrong)

constructClassTheory

public TheoryDeclaration constructClassTheory(ClassSymbol csymbol)

Construct a theory declaration for the denoted class.

Parameters:

csymbol - the symbol of the class

Returns:

the declaration (null, on error)