gov.nasa.jpf.symbc.veritesting.VeritestingUtil

Class ExprUtil

java.lang.Object

gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ExprUtil

public class ExprUtil
extends java.lang.Object

A utility class that provides some methods from SPF to Green and vise versa.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	ExprUtil.SatResult

Constructor Summary

Constructors

Constructor and Description
ExprUtil()

Method Summary

Modifier and Type	Method and Description
static java.lang.String	AstToString(za.ac.sun.cs.green.expr.Expression expression) Pretty print method to print Green expression.
static Stmt	compose(Stmt s1, Stmt s2, boolean allowBothNull)
static za.ac.sun.cs.green.expr.Expression	createGreenVar(java.lang.String type, java.lang.String varId) Creates a Green variable depending on its type.
static ExprUtil.SatResult	foldBooleanOp(za.ac.sun.cs.green.expr.Operation operation)
static java.lang.String	getConstantType(za.ac.sun.cs.green.expr.Expression expr)
static java.lang.String	getGreenVariableType(za.ac.sun.cs.green.expr.Expression expr)
static gov.nasa.jpf.symbc.numeric.Expression	greenToSPFExpression(za.ac.sun.cs.green.expr.Expression greenExpression) Translates Green Expession to SPF.
static boolean	isConstant(za.ac.sun.cs.green.expr.Expression expr)
static boolean	isPCSat(gov.nasa.jpf.symbc.numeric.PathCondition pc)
static ExprUtil.SatResult	isSatGreenExpression(za.ac.sun.cs.green.expr.Expression expression)
static boolean	isSatisfiable(gov.nasa.jpf.symbc.numeric.PathCondition pc)
static boolean	isVariable(za.ac.sun.cs.green.expr.Expression expr)
static za.ac.sun.cs.green.expr.Expression	SPFToGreenExpr(gov.nasa.jpf.symbc.numeric.Expression spfExp) Translates an SPF expression to a Green Expression.
static za.ac.sun.cs.green.expr.Expression	translateNotExpr(za.ac.sun.cs.green.expr.Operation op)

Methods inherited from class java.lang.Object

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

Constructor Detail

ExprUtil

public ExprUtil()

Method Detail

SPFToGreenExpr

public static za.ac.sun.cs.green.expr.Expression SPFToGreenExpr(gov.nasa.jpf.symbc.numeric.Expression spfExp)

Translates an SPF expression to a Green Expression.

Parameters:

spfExp - SPF Expression

Returns:

Green Expression.

AstToString

public static java.lang.String AstToString(za.ac.sun.cs.green.expr.Expression expression)

Pretty print method to print Green expression.

Parameters:

expression - Green expression.

Returns:

String of Green Expression.

greenToSPFExpression

public static gov.nasa.jpf.symbc.numeric.Expression greenToSPFExpression(za.ac.sun.cs.green.expr.Expression greenExpression)

Translates Green Expession to SPF.

Parameters:

greenExpression - A Green expression to be translated to SPF.

Returns:

SPF expression.

createGreenVar

public static za.ac.sun.cs.green.expr.Expression createGreenVar(java.lang.String type,
                                                                java.lang.String varId)

Creates a Green variable depending on its type.

Parameters:

type - Type of the variable.

varId - Name of the variable.

Returns:

A Green variable.

isConstant

public static boolean isConstant(za.ac.sun.cs.green.expr.Expression expr)

isVariable

public static boolean isVariable(za.ac.sun.cs.green.expr.Expression expr)

getConstantType

public static java.lang.String getConstantType(za.ac.sun.cs.green.expr.Expression expr)

getGreenVariableType

public static java.lang.String getGreenVariableType(za.ac.sun.cs.green.expr.Expression expr)

isPCSat

public static boolean isPCSat(gov.nasa.jpf.symbc.numeric.PathCondition pc)
                       throws StaticRegionException

Throws:

StaticRegionException

isSatisfiable

public static boolean isSatisfiable(gov.nasa.jpf.symbc.numeric.PathCondition pc)
                             throws StaticRegionException

Throws:

StaticRegionException

isSatGreenExpression

public static ExprUtil.SatResult isSatGreenExpression(za.ac.sun.cs.green.expr.Expression expression)

foldBooleanOp

public static ExprUtil.SatResult foldBooleanOp(za.ac.sun.cs.green.expr.Operation operation)

translateNotExpr

public static za.ac.sun.cs.green.expr.Expression translateNotExpr(za.ac.sun.cs.green.expr.Operation op)

compose

public static Stmt compose(Stmt s1,
                           Stmt s2,
                           boolean allowBothNull)