Immediately transition to a RunningState. On the next execution step, the simulator will interpret the next basic block.

Transfer control to the given resolved jump, after first checking for any pending symbolic merges at the destination of the jump.

Perform a conditional branch on the given predicate. If the predicate is symbolic, this will record a symbolic branch state.

Execute the next branch of a sequence of branch cases. These arise from the implementation of the VariantElim construct. The predicates are expected to be mutually disjoint. However, the construct still has well defined semantics even in the case where they overlap; in this case, the first branch with a true Pred is taken. In other words, each branch assumes the negation of all the predicates of branches appearing before it.

In the final default case (corresponding to an empty list of branches), a VariantOptionsExhausted abort will be executed.

Return a value from current Crucible execution.

Immediately transtition to an OverrideState. On the next execution step, the simulator will execute the given override.

Immediately transition to an AbortState. On the next execution step, the simulator will unwind the SimState and resolve the abort.

Abort the current thread of execution with an error. This adds a proof obligation that requires the current execution path to be infeasible, and unwids to the nearest branch point to resume.

Abort the current thread of execution with an error. This adds a proof obligation that requires the current execution path to be infeasible, and unwids to the nearest branch point to resume.

Perform a single instance of path merging at a join point. This will resume an alternate branch, if it is pending, or merge result values if a completed branch has alread reached this point. If there are no pending merge points at this location, continue executing by transfering control to the given target.

Branch with a merge point inside this frame.

Resolve the return value, and begin executing in the caller's context again.

Resume a paused frame.

Run rest of execution given a value from value context and an aborted result.

The result of resolving a function call.

Type parameters:

• p: see cruciblePersonality
• sym: instance of IsSymInterface
• ext: language extension, see Lang.Crucible.CFG.Extension
• ret: CrucibleType of the return value

This exception is thrown if a FnHandle cannot be resolved to a callable function. This usually indicates a programming error, but might also be used to allow on-demand function loading.

The ProgramLoc argument references the call site for the unresolved function call.

The [SomeFrame] argument is the active call stack at the time of the exception.

Given a set of function bindings, a function- value (which is possibly a closure) and a collection of arguments, resolve the identity of the function to call, and set it up to be called.

Will throw an UnresolvableFunction exception if the underlying function handle is not found in the FunctionBindings map.

Abort the current execution and roll back to the nearest symbolic branch point. When verbosity is 3 or more, a message will be logged indicating the reason for the abort.

The default abort handler calls this function.

Abort the current execution and roll back to the nearest symbolic branch point.

The default abort handler calls abortExecAndLog.

Replace the given frame with a new frame. Succeeds only if there are no pending symbolic merge points.

Returns true if tree contains a single non-aborted execution.

Attempt to unwind a frame context into a value context. This succeeds only if there are no pending symbolic merges.

Create a tree that contains just a single path with no branches.

All branch conditions are converted to assertions.

Return the context of the current top frame.