package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install 

dune-project
 Dependency

goblint.in.tum.de Readme Changelog Edit opam file Versions (9)

Authors

  1. V
    Vesal Vojdani
  2. K
    Kalmer Apinis
  3. R
    Ralf Vogler
  4. M
    Michael Schwarz
  5. J
    Julian Erhard
  6. S
    Simmo Saan

Maintainers

  1. M
    Michael Schwarz <michael.schwarz93@gmail.com>
  2. S
    Simmo Saan <simmo.saan@gmail.com>
  3. R
    Ralf Vogler <ralf.vogler@gmail.com>

Sources

goblint-1.1.1.tbz
sha256=999272bfbd3b9b96fcd58987b237ac6e9fa6d92ef935cc89f1ea2b4205185141
sha512=f3bf6ab71cf8c258d3290da4bf9f6fe42d7c671822e0efeb0fc50afdff078ab15e352237e5c1db31c5aa3a9d430691268ed2e5e00da10f2615835f672f91683d

doc/goblint.lib/CompareCIL/index.html

Module CompareCIL

include module type of struct include CompareAST end
exception NoGlobalIdentifier of Cil.global
include module type of struct include CompareCFG end
include module type of struct include CompareAST end
type global_type = CompareAST.global_type =
  1. | Fun
  2. | Decl
  3. | Var
  4. | Other
and global_identifier = CompareAST.global_identifier = {
  1. name : string;
  2. global_t : global_type;
}
val compare_global_type : global_type -> global_type -> Ppx_deriving_runtime.int
val compare_global_identifier : global_identifier -> global_identifier -> Ppx_deriving_runtime.int
exception NoGlobalIdentifier of Cil.global
val identifier_of_global : Cil.global -> global_identifier
module GlobalMap = CompareCFG.GlobalMap
val eq_list : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val eqB : Cil.block -> Cil.block -> bool
val eqS : Cil.stmt -> Cil.stmt -> bool
val print : Pretty.doc -> unit
val compare_name : string -> string -> bool
val eq_constant : Cil.constant -> Cil.constant -> bool
val eq_exp : Cil.exp -> Cil.exp -> bool
val eq_lhost : Cil.lhost -> Cil.lhost -> bool
val global_typ_acc : (Cil.typ * Cil.typ) list ref
val mem_typ_acc : Cil.typ -> Cil.typ -> (Cil.typ * Cil.typ) list -> bool
val pretty_length : unit -> (Cil.typ * Cil.typ) list -> Pretty.doc
val eq_typ_acc : Cil.typ -> Cil.typ -> (Cil.typ * Cil.typ) list -> bool
val eq_typ : Cil.typ -> Cil.typ -> bool
val eq_eitems : (string * Cil.exp * Cil.location) -> (string * Cil.exp * Cil.location) -> bool
val eq_enuminfo : Cil.enuminfo -> Cil.enuminfo -> bool
val eq_args : (Cil.typ * Cil.typ) list -> (string * Cil.typ * Cil.attributes) -> (string * Cil.typ * Cil.attributes) -> bool
val eq_attrparam : Cil.attrparam -> Cil.attrparam -> bool
val eq_attribute : Cil.attribute -> Cil.attribute -> bool
val eq_varinfo : Cil.varinfo -> Cil.varinfo -> bool
val eq_compinfo : Cil.compinfo -> Cil.compinfo -> (Cil.typ * Cil.typ) list -> bool
val eq_fieldinfo : Cil.fieldinfo -> Cil.fieldinfo -> (Cil.typ * Cil.typ) list -> bool
val eq_offset : Cil.offset -> Cil.offset -> bool
val eq_lval : Cil.lval -> Cil.lval -> bool
val eq_instr : Cil.instr -> Cil.instr -> bool
val eq_label : Cil.label -> Cil.label -> bool
val eq_stmt_with_location : (Cil.stmt * Cil.fundec) -> (Cil.stmt * Cil.fundec) -> bool
val eq_stmtkind : ?cfg_comp:bool -> (Cil.stmtkind * Cil.fundec) -> (Cil.stmtkind * Cil.fundec) -> bool
val eq_stmt : ?cfg_comp:bool -> (Cil.stmt * Cil.fundec) -> (Cil.stmt * Cil.fundec) -> bool
val eq_block : (Cil.block * Cil.fundec) -> (Cil.block * Cil.fundec) -> bool
val eq_init : Cil.init -> Cil.init -> bool
val eq_initinfo : Cil.initinfo -> Cil.initinfo -> bool
val eq_node : (MyCFG.node * Cil.fundec) -> (MyCFG.node * Cil.fundec) -> bool
val eq_edge : MyCFG.edge -> MyCFG.edge -> bool
val eq_edge_list : MyCFG.edge list -> MyCFG.edge list -> bool
val to_edge_list : ('a * 'b) list -> 'b list
module NH = CompareCFG.NH
module NTH = CompareCFG.NTH
val compareCfgs : (module MyCFG.CfgForward) -> (module MyCFG.CfgForward) -> CilType.Fundec.t -> CilType.Fundec.t -> unit NTH.t * unit NH.t
val reexamine : CilType.Fundec.t -> CilType.Fundec.t -> unit NTH.t -> unit NH.t -> (module MyCFG.CfgForward) -> (module MyCFG.CfgForward) -> NTH.key Seq.t * NH.key Seq.t * NH.key Seq.t
val compareFun : (module MyCFG.CfgForward) -> (module MyCFG.CfgForward) -> CilType.Fundec.t -> CilType.Fundec.t -> NTH.key list * NH.key list * NH.key list
type nodes_diff = {
  1. unchangedNodes : (MyCFG.node * MyCFG.node) list;
  2. primObsoleteNodes : MyCFG.node list;
    (*

    primary obsolete nodes -> all obsolete nodes are reachable from these

    *)
  3. primNewNodes : MyCFG.node list;
    (*

    primary new nodes -> all differing nodes in the new CFG are reachable from these

    *)
}
type changed_global = {
  1. old : Cil.global;
  2. current : Cil.global;
  3. unchangedHeader : bool;
  4. diff : nodes_diff option;
}
type change_info = {
  1. mutable changed : changed_global list;
  2. mutable unchanged : Cil.global list;
  3. mutable removed : Cil.global list;
  4. mutable added : Cil.global list;
}
val empty_change_info : unit -> change_info
val eqF : Cil.fundec -> Cil.fundec -> (MyCFG.cfg * MyCFG.cfg) option -> bool * bool * nodes_diff option
val eq_glob : Cil.global -> Cil.global -> (MyCFG.cfg * MyCFG.cfg) option -> bool * bool * nodes_diff option
val compareCilFiles : Cil.file -> Cil.file -> change_info