package goblint
Install
dune-project
Dependency
Authors
Maintainers
Sources
sha256=20d5b7332a9f6072ab9ba86c4a53b898eaf681286c56a8805c41850bbf3ddf41
sha512=7c7685cfcd9aa866bc40e813df2bfcb3c79b3d40e615d8d6d0939c5798b9d70dd7f2ba87a741f5ba0ce891e9d254627207fb28057f1f2f6611e4e0d128fd6a71
doc/goblint.common/Edge/index.html
Module Edge
CFG edge. Corresponds to a (primitive) program statement between program points (and their states).
type asm_out = (string option * string * CilType.Lval.t) listval equal_asm_out : asm_out -> asm_out -> Ppx_deriving_runtime.boolval compare_asm_out : asm_out -> asm_out -> Ppx_deriving_runtime.intval hash_asm_out : asm_out -> intval asm_out_to_yojson : asm_out -> Yojson.Safe.ttype asm_in = (string option * string * CilType.Exp.t) listval equal_asm_in : asm_in -> asm_in -> Ppx_deriving_runtime.boolval compare_asm_in : asm_in -> asm_in -> Ppx_deriving_runtime.intval hash_asm_in : asm_in -> intval asm_in_to_yojson : asm_in -> Yojson.Safe.tval _ : asm_in -> Yojson.Safe.ttype t = | Assign of CilType.Lval.t * CilType.Exp.t(*Assignments lval = exp
*)| Proc of CilType.Lval.t option * CilType.Exp.t * CilType.Exp.t list(*Function calls of the form lva = fexp (e1, e2, ...)
*)| Entry of CilType.Fundec.t(*Entry edge that relates function declaration to function body. You can use * this to initialize the local variables.
*)| Ret of CilType.Exp.t option * CilType.Fundec.t(*Return edge is between the return statement, which may optionally contain * a return value, and the function. The result of the call is then * transferred to the function node!
*)| Test of CilType.Exp.t * bool(*The true-branch or false-branch of a conditional exp
*)| ASM of string list * asm_out * asm_in(*Inline assembly statements, and the annotations for output and input * variables.
*)| VDecl of CilType.Varinfo.t(*VDecl edge for the variable in varinfo. Whether such an edge is there for all * local variables or only when it is not possible to pull the declaration up, is * determined by alwaysGenerateVarDecl in cabs2cil.ml in CIL. One case in which a VDecl * is always there is for VLA. If there is a VDecl edge, it is where the declaration originally * appeared
*)| Skip(*This is here for historical reasons. I never use Skip edges!
*)
val equal : t -> t -> Ppx_deriving_runtime.boolval compare : t -> t -> Ppx_deriving_runtime.intval hash : t -> intval pretty : unit -> t -> GoblintCil.Pretty.docval pretty_plain : unit -> t -> GoblintCil.Pretty.docval to_yojson : t -> [> `Assoc of (string * Yojson.Safe.t) list ]