forge.translate
Class SymbolicExecutor

java.lang.Object
  forge.translate.ExprTranslator
      forge.translate.SymbolicExecutor

public final class SymbolicExecutor
extends ExprTranslator

Symbolically executes statements.

Author:

Greg Dennis (gdennis@mit.edu)

Nested Class Summary

class	SymbolicExecutor.AssignHook Callback hook for execute(AssignStmt) method.
class	SymbolicExecutor.BranchHook Callback hook for the merge method.
class	SymbolicExecutor.CreateHook Callback hook for execute(CreateStmt) method.
class	SymbolicExecutor.SpecHook Callback hook for execute(AssignStmt) method.

Constructor Summary

SymbolicExecutor(SEStrategy strategy, Environment env, forge.translate.SliceLog slices)

Method Summary

java.util.List<kodkod.ast.Formula>	assumes()
void	execute(AssignStmt stmt)
void	execute(CreateStmt stmt)
void	execute(SpecStmt stmt)
static SymbolicExecutor	initialize(SEStrategy strategy, ForgeCFG cfg, boolean logSlices)
void	merge(BranchStmt stmt, SymbolicExecutor seThen, SymbolicExecutor seElse) Merge symbolic execution from both sides of a branch.
forge.translate.SliceLog	slices()
SEStrategy	strategy()

Methods inherited from class forge.translate.ExprTranslator

env, model, pinOldExpr, program, toExpr, toExpr, toForm, toInt, unpinOldExprs

Methods inherited from class java.lang.Object

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

Constructor Detail

SymbolicExecutor

public SymbolicExecutor(SEStrategy strategy,
                        Environment env,
                        forge.translate.SliceLog slices)

Method Detail

initialize

public static SymbolicExecutor initialize(SEStrategy strategy,
                                          ForgeCFG cfg,
                                          boolean logSlices)

strategy

public SEStrategy strategy()

assumes

public java.util.List<kodkod.ast.Formula> assumes()

slices

public forge.translate.SliceLog slices()

execute

public void execute(AssignStmt stmt)

execute

public void execute(CreateStmt stmt)

execute

public void execute(SpecStmt stmt)

merge

public void merge(BranchStmt stmt,
                  SymbolicExecutor seThen,
                  SymbolicExecutor seElse)

Merge symbolic execution from both sides of a branch.