class AAMAACP4F[Exp, Abs, Addr, Time] extends EvalKontMachine[Exp, Abs, Addr, Time]
AAM/AAC/P4F techniques combined in a single machine abstraction
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- AAMAACP4F
- EvalKontMachine
- AbstractMachine
- AnyRef
- Any
Implicitly
- by any2stringadd
- by StringFormat
- by Ensuring
- by ArrowAssoc
- Hide All
- Show All
Visibility
- Public
- All
Instance Constructors
- new AAMAACP4F(strategy: KAllocStrategy)(implicit arg0: Expression[Exp], arg1: JoinLattice[Abs], arg2: Address[Addr], arg3: Timestamp[Time])
Type Members
- case class AACKontAddress(e2: Exp, env2: Environment[Addr], control: AAMAACP4F.Control, store: Store[Addr, Abs], t: Time) extends KontAddr with Product with Serializable
- case class AAMAACP4FOutput(halted: Set[State], store: Store[Addr, Abs], numberOfStates: Int, time: Double, graph: G, timedOut: Boolean) extends Output with Product with Serializable
- case class AAMKontAddress(e2: Exp, t: Time) extends KontAddr with Product with Serializable
- type G = Option[Graph[State, Unit, Context]]
- case class GlobalStore(store: DeltaStore[Addr, Abs], delta: Map[Addr, Abs]) extends Product with Serializable
- trait KontAddr extends AnyRef
- case class P4FKontAddress(e2: Exp, env2: Environment[Addr], t: Time) extends KontAddr with Product with Serializable
- case class State(control: AAMAACP4F.Control, a: KontAddr, t: Time) extends Product with Serializable
-
trait
Output extends AnyRef
The output of the abstract machine
The output of the abstract machine
- Definition Classes
- AbstractMachine
-
trait
Control extends AnyRef
The control component of the machine
The control component of the machine
- Definition Classes
- EvalKontMachine
-
case class
ControlError(err: SemanticError) extends Control with Product with Serializable
Or an error component, in case an error is reached (e.g., incorrect number of arguments in a function call)
Or an error component, in case an error is reached (e.g., incorrect number of arguments in a function call)
- Definition Classes
- EvalKontMachine
-
case class
ControlEval(exp: Exp, env: Environment[Addr]) extends Control with Product with Serializable
It can either be an eval component, where an expression needs to be evaluated in an environment
It can either be an eval component, where an expression needs to be evaluated in an environment
- Definition Classes
- EvalKontMachine
-
case class
ControlKont(v: Abs) extends Control with Product with Serializable
Or it can be a continuation component, where a value has been reached and a continuation should be popped from the stack to continue the evaluation
Or it can be a continuation component, where a value has been reached and a continuation should be popped from the stack to continue the evaluation
- Definition Classes
- EvalKontMachine
Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
- def +(other: String): String
- def ->[B](y: B): (AAMAACP4F[Exp, Abs, Addr, Time], B)
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate() @throws( ... )
- def ensuring(cond: (AAMAACP4F[Exp, Abs, Addr, Time]) ⇒ Boolean, msg: ⇒ Any): AAMAACP4F[Exp, Abs, Addr, Time]
- def ensuring(cond: (AAMAACP4F[Exp, Abs, Addr, Time]) ⇒ Boolean): AAMAACP4F[Exp, Abs, Addr, Time]
- def ensuring(cond: Boolean, msg: ⇒ Any): AAMAACP4F[Exp, Abs, Addr, Time]
- def ensuring(cond: Boolean): AAMAACP4F[Exp, Abs, Addr, Time]
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
eval(exp: Exp, sem: Semantics[Exp, Abs, Addr, Time], genGraph: Boolean, timeout: Timeout): Output
Evaluate a program represented by an expression, under the given semantics.
Evaluate a program represented by an expression, under the given semantics. A graph can be generated if @genGraph is true, and a timeout can be given.
- Definition Classes
- AAMAACP4F → AbstractMachine
- def formatted(fmtstr: String): String
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- def kalloc(state: State, e: Exp, env: Environment[Addr], store: Store[Addr, Abs], t: Time): Product with Serializable with KontAddr
-
def
name: String
The name of the abstract machine
The name of the abstract machine
- Definition Classes
- AAMAACP4F → AbstractMachine
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- implicit val stateWithKey: WithKey[State] { type K = AAMAACP4F.this.KontAddr }
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toString(): String
- Definition Classes
- AnyRef → Any
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
- def →[B](y: B): (AAMAACP4F[Exp, Abs, Addr, Time], B)
- object HaltKontAddress extends KontAddr with Product with Serializable
- object KontAddr
- object State extends Serializable
-
object
Control
- Definition Classes
- EvalKontMachine