Legend:
Library
Module
Module type
Parameter
Class
Class type
A control transfer operation.
Jmp is the only way to transfer control from block to block. Jumps are guarded with conditions. The jump should be taken only if its condition is evaluated to true. When control flow reaches the end of block it should take the first jump with true condition. If there is no such jump, then program stops.
Jumps are further subdivided into categories:
goto - is a local control transfer instruction. The label can be only local to subroutine;
call - transfer a control to another subroutine. A call contains a continuation, i.e., a label to which we're hoping to return after subroutine returns the control to us. Of course, called subroutine can in general return to another position, or not to return at all.
ret - performs a return from subroutine
int - calls to interrupt subroutine. If interrupt returns, then continue with the provided label.
val reify :
?tid:tid->?cnd:Bap_core_theory.Theory.Bool.t Bap_core_theory.Theory.value->?alt:dst->?dst:dst->unit ->t
reify () reifies inputs into a jump term.
Calls and interrupt subroutines invocations are represented with two edges: the normal edge (denoted dst) is the intra-procedural edge which connects the callsite with the fall-through destination (if such exists) and an alternative destination (denoted with alt) which represents an inter-procedural destination between the callsite and the call destination.
parametercnd
is a core theory term that denotes the guard condition of a conditional jump.
parameteralt
is the alternative control flow destination.
parameterdst
is the direct control flow destination
@tid is the jump identifier, if not specified a fresh new identifier is created.
val guard :
t->Bap_core_theory.Theory.Bool.t Bap_core_theory.Theory.value option
guard jmp if jmp is conditional, returns its condition.
val with_guard :
t->Bap_core_theory.Theory.Bool.t Bap_core_theory.Theory.value option->t
with_guard jmp cnd updates the jump condition of jmp.