class ConcolicEngine extends SymbolicInterpreter
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- ConcolicEngine
- SymbolicInterpreter
- Interpreter
- AnyRef
- Any
- Hide All
- Show All
Visibility
- Public
- All
Instance Constructors
- new ConcolicEngine(program: AProgram)(implicit declData: DeclarationData)
Type Members
-
type
Env = Map[ADeclaration, SymbolicValues.Location]
- Definition Classes
- Interpreter
- case class ExFailure(s: ConcolicEngine.ConcolicState, message: String) extends ExecutionResult with Product with Serializable
- case class ExSuccess(s: ConcolicEngine.ConcolicState, value: Int) extends ExecutionResult with Product with Serializable
- abstract class ExecutionResult extends AnyRef
-
type
Extra = ConcolicState
- Definition Classes
- SymbolicInterpreter → Interpreter
-
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
-
class
ExecutionError extends TipProgramException
- Definition Classes
- Interpreter
-
case class
Store(content: Map[ReferenceValue, Value], extra: Extra) extends Product with Serializable
- Definition Classes
- Interpreter
Value Members
-
val
capturedOut: StringBuilder
- Definition Classes
- Interpreter
-
def
errorAccessMissingField(loc: Loc, rec: SymbolicValues.RecordValue, field: String, store: Store): Nothing
- Definition Classes
- Interpreter
-
def
errorAccessNonRecord(loc: Loc, x: SymbolicValues.EValue, store: Store): Nothing
- Definition Classes
- Interpreter
-
def
errorArithmeticOnNonInt(loc: Loc, op: BinaryOperator, store: Store): Nothing
- Definition Classes
- Interpreter
-
def
errorCallNotFunction(loc: Loc, funValue: SymbolicValues.EValue, store: Store): Nothing
- Definition Classes
- Interpreter
-
def
errorConditionNotInt(loc: Loc, store: Store): Nothing
- Definition Classes
- Interpreter
-
def
errorDerefNotPointer(loc: Loc, x: SymbolicValues.EValue, store: Store): Nothing
- Definition Classes
- Interpreter
-
def
errorErrorNonInt(loc: Loc, v: SymbolicValues.EValue, store: Store): Nothing
- Definition Classes
- Interpreter
-
def
errorInputNotInt(loc: Loc, store: Store): Nothing
- Definition Classes
- Interpreter
-
def
errorNullDereference(loc: Loc, store: Store): Nothing
- Definition Classes
- Interpreter
-
def
errorOutputNotInt(loc: Loc, store: Store): Nothing
- Definition Classes
- Interpreter
-
def
errorReturnNotInt(loc: Loc, fun: AFunDeclaration, store: Store): Nothing
- Definition Classes
- Interpreter
-
def
errorUninitializedLocation(loc: Loc, store: Store): Nothing
- Definition Classes
- Interpreter
-
def
errorWriteFieldRecord(loc: Loc, x: SymbolicValues.EValue, store: Store): Nothing
- Definition Classes
- Interpreter
-
val
log: Logger
- Definition Classes
- ConcolicEngine → Interpreter
- def newInputs(symbols: List[Symbol], lastNode: ExecutionTree, root: ExecutionTreeRoot): Option[List[Int]]
- def nextExplorationTarget(lastExplored: ExecutionTree, root: ExecutionTreeRoot): Option[(Branch, Boolean)]
- val program: AProgram
-
def
semp(): SymbolicValues.IntValue
- Definition Classes
- SymbolicInterpreter
-
def
semp(ct: ExecutionTree, inputs: List[Int]): (SymbolicValues.IntValue, Store)
- Definition Classes
- SymbolicInterpreter
-
def
semp(initEnv: Env, initStore: Store): (SymbolicValues.IntValue, Store)
Semantics for programs.
-
val
spec: SymbolicValues.type
- Definition Classes
- SymbolicInterpreter → Interpreter
- def test(budget: Int = 20): Unit