package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install

Dune Dependency

Authors

Maintainers

Sources

goblint-2.1.0.tbz
sha256=bfc412ec2e447eaef6f4f83892e3511ebf305593cb00561c1406be3ae8bf48e9
sha512=5f2a162e5f36bffafc9836b0d18b5b2808cecfa6bf68f83bb7d1e8b9947ac74cf07776eb09274b4b29d55c897a45a10768f0d9ed25810cf6ba2409c525e4cd4d

doc/goblint.lib/Goblint_lib/Edge/index.html

Module Goblint_lib.Edge

type asm_out = (string option * string * CilType.Lval.t) list
val equal_asm_out : asm_out -> asm_out -> Ppx_deriving_runtime.bool
val compare_asm_out : asm_out -> asm_out -> Ppx_deriving_runtime.int
val hash_asm_out : asm_out -> int
val asm_out_to_yojson : asm_out -> Yojson.Safe.t
type asm_in = (string option * string * CilType.Exp.t) list
val equal_asm_in : asm_in -> asm_in -> Ppx_deriving_runtime.bool
val compare_asm_in : asm_in -> asm_in -> Ppx_deriving_runtime.int
val hash_asm_in : asm_in -> int
val asm_in_to_yojson : asm_in -> Yojson.Safe.t
type t =
  1. | Assign of CilType.Lval.t * CilType.Exp.t
    (*

    Assignments lval = exp

    *)
  2. | Proc of CilType.Lval.t option * CilType.Exp.t * CilType.Exp.t list
    (*

    Function calls of the form lva = fexp (e1, e2, ...)

    *)
  3. | Entry of CilType.Fundec.t
    (*

    Entry edge that relates function declaration to function body. You can use * this to initialize the local variables.

    *)
  4. | 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!

    *)
  5. | Test of CilType.Exp.t * bool
    (*

    The true-branch or false-branch of a conditional exp

    *)
  6. | ASM of string list * asm_out * asm_in
    (*

    Inline assembly statements, and the annotations for output and input * variables.

    *)
  7. | 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

    *)
  8. | Skip
    (*

    This is here for historical reasons. I never use Skip edges!

    *)
val equal : t -> t -> Ppx_deriving_runtime.bool
val compare : t -> t -> Ppx_deriving_runtime.int
val hash : t -> int
val to_yojson : t -> Yojson.Safe.t
val _ : t -> Yojson.Safe.t
val pretty : unit -> t -> GoblintCil.Pretty.doc
val pretty_plain : unit -> t -> GoblintCil.Pretty.doc
OCaml

Innovation. Community. Security.