gov.nasa.jpf.symbc.veritesting.ast.transformations.linearization

Class LinearizationVisitor

java.lang.Object

gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

gov.nasa.jpf.symbc.veritesting.ast.transformations.linearization.LinearizationVisitor

All Implemented Interfaces:

AstVisitor<Stmt>, ExprVisitor<za.ac.sun.cs.green.expr.Expression>

public class LinearizationVisitor
extends AstMapVisitor

Linearalize region statement by removing "If" Statements and embedding statements on the "then" and the "else" side, to become one stream of composition statements. Assumptions: there are no more \phi functions, and every join // point for variable definitions is represented by a \Gamma function

Field Summary

Fields inherited from class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

eva, exprVisitor

Constructor Summary

Constructors

Constructor and Description
LinearizationVisitor()

Method Summary

Modifier and Type	Method and Description
Stmt	visit(IfThenElseStmt stmt)

Methods inherited from class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit

Methods inherited from class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit

Methods inherited from class java.lang.Object

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

Constructor Detail

LinearizationVisitor

public LinearizationVisitor()

Method Detail

visit

public Stmt visit(IfThenElseStmt stmt)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor