c

tip.concolic

ConcolicEngine

class ConcolicEngine extends SymbolicInterpreter

Linear Supertypes
SymbolicInterpreter, Interpreter, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. ConcolicEngine
  2. SymbolicInterpreter
  3. Interpreter
  4. AnyRef
  5. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new ConcolicEngine(program: AProgram)(implicit declData: DeclarationData)

Type Members

  1. type Env = Map[ADeclaration, SymbolicValues.Location]
    Definition Classes
    Interpreter
  2. case class ExFailure(s: ConcolicEngine.ConcolicState, message: String) extends ExecutionResult with Product with Serializable
  3. case class ExSuccess(s: ConcolicEngine.ConcolicState, value: Int) extends ExecutionResult with Product with Serializable
  4. abstract class ExecutionResult extends AnyRef
  5. type Extra = ConcolicState
    Definition Classes
    SymbolicInterpreter → Interpreter
  6. case class ConcolicState(symbols: List[Symbol] = Nil, ct: ExecutionTree, counter: Int = 0, inputs: List[Int], usedInputs: List[Int] = Nil) extends Product with Serializable
    Definition Classes
    SymbolicInterpreter
  7. class ExecutionError extends TipProgramException
    Definition Classes
    Interpreter
  8. case class Store(content: Map[ReferenceValue, Value], extra: Extra) extends Product with Serializable
    Definition Classes
    Interpreter

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  5. def branchTaken(guard: AExpr, value: SymbolicValues.EValue, branch: Boolean, store: Store): Store
    Attributes
    protected
    Definition Classes
    SymbolicInterpreter → Interpreter
  6. val capturedOut: StringBuilder
    Definition Classes
    Interpreter
  7. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native() @IntrinsicCandidate()
  8. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  9. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  10. def errorAccessMissingField(loc: Loc, rec: SymbolicValues.RecordValue, field: String, store: Store): Nothing
    Definition Classes
    Interpreter
  11. def errorAccessNonRecord(loc: Loc, x: SymbolicValues.EValue, store: Store): Nothing
    Definition Classes
    Interpreter
  12. def errorArithmeticOnNonInt(loc: Loc, op: BinaryOperator, store: Store): Nothing
    Definition Classes
    Interpreter
  13. def errorCallNotFunction(loc: Loc, funValue: SymbolicValues.EValue, store: Store): Nothing
    Definition Classes
    Interpreter
  14. def errorConditionNotInt(loc: Loc, store: Store): Nothing
    Definition Classes
    Interpreter
  15. def errorDerefNotPointer(loc: Loc, x: SymbolicValues.EValue, store: Store): Nothing
    Definition Classes
    Interpreter
  16. def errorErrorNonInt(loc: Loc, v: SymbolicValues.EValue, store: Store): Nothing
    Definition Classes
    Interpreter
  17. def errorInputNotInt(loc: Loc, store: Store): Nothing
    Definition Classes
    Interpreter
  18. def errorNullDereference(loc: Loc, store: Store): Nothing
    Definition Classes
    Interpreter
  19. def errorOutputNotInt(loc: Loc, store: Store): Nothing
    Definition Classes
    Interpreter
  20. def errorReturnNotInt(loc: Loc, fun: AFunDeclaration, store: Store): Nothing
    Definition Classes
    Interpreter
  21. def errorUninitializedLocation(loc: Loc, store: Store): Nothing
    Definition Classes
    Interpreter
  22. def errorWriteFieldRecord(loc: Loc, x: SymbolicValues.EValue, store: Store): Nothing
    Definition Classes
    Interpreter
  23. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @IntrinsicCandidate()
  24. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @IntrinsicCandidate()
  25. def input(exp: AExpr, env: Env, store: Store): (SymbolicValues.EValue, Store)

    Takes an integer input from stdin.

    Takes an integer input from stdin.

    Attributes
    protected
    Definition Classes
    SymbolicInterpreter → Interpreter
  26. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  27. val log: Logger
    Definition Classes
    ConcolicEngine → Interpreter
  28. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  29. def newInputs(symbols: List[Symbol], lastNode: ExecutionTree, root: ExecutionTreeRoot): Option[List[Int]]
  30. def nextExplorationTarget(lastExplored: ExecutionTree, root: ExecutionTreeRoot): Option[(Branch, Boolean)]
  31. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @IntrinsicCandidate()
  32. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @IntrinsicCandidate()
  33. val program: AProgram
  34. def semc(stm: AStmt, env: Env, store: Store): (Env, Store)

    Semantics for statements (including local variable declarations).

    Semantics for statements (including local variable declarations).

    stm

    the statement to execute

    env

    the initial environment

    store

    the initial store

    returns

    the resulting environment and store

    Attributes
    protected
    Definition Classes
    Interpreter
  35. def semeref(exp: FieldAssignable, env: Env, store: Store): (SymbolicValues.ReferenceValue, String, Store)

    Semantics for field lvalue expressions.

    Semantics for field lvalue expressions.

    exp

    the lvalue expression to execute

    env

    the environment

    store

    the initial store

    returns

    the resulting location, field, and store

    Attributes
    protected
    Definition Classes
    Interpreter
  36. def semeref(exp: ReferenceAssignable, env: Env, store: Store): (SymbolicValues.ReferenceValue, Store)

    Semantics for ordinary lvalue expressions.

    Semantics for ordinary lvalue expressions.

    exp

    the lvalue expression to execute

    env

    the environment

    store

    the initial store

    returns

    the resulting location and store

    Attributes
    protected
    Definition Classes
    Interpreter
  37. def semeright(exp: AExpr, env: Env, store: Store): (SymbolicValues.EValue, Store)

    Semantics for right-hand-side expressions.

    Semantics for right-hand-side expressions.

    exp

    the expression to execute

    env

    the environment

    store

    the initial store

    returns

    the resulting value and store

    Attributes
    protected
    Definition Classes
    Interpreter
  38. def semp(): SymbolicValues.IntValue
    Definition Classes
    SymbolicInterpreter
  39. def semp(ct: ExecutionTree, inputs: List[Int]): (SymbolicValues.IntValue, Store)
    Definition Classes
    SymbolicInterpreter
  40. def semp(initEnv: Env, initStore: Store): (SymbolicValues.IntValue, Store)

    Semantics for programs.

    Semantics for programs.

    returns

    the resulting value

    Definition Classes
    Interpreter
  41. val spec: SymbolicValues.type
    Definition Classes
    SymbolicInterpreter → Interpreter
  42. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  43. def test(budget: Int = 20): Unit
  44. def toString(): String
    Definition Classes
    AnyRef → Any
  45. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  46. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()
  47. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] ) @Deprecated
    Deprecated

Inherited from SymbolicInterpreter

Inherited from Interpreter

Inherited from AnyRef

Inherited from Any

Ungrouped