package goblint

You can search for identifiers within the package.

in-package search v0.2.0

Static analysis framework for C

Install

Dune Dependency

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

Authors

Maintainers

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 =

| Fun
| Decl
| Var
| Other

and global_identifier = CompareAST.global_identifier = {

name : string;
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 = {

unchangedNodes : (MyCFG.node * MyCFG.node) list;
primObsoleteNodes : MyCFG.node list;
(*
primary obsolete nodes -> all obsolete nodes are reachable from these
*)
primNewNodes : MyCFG.node list;
(*
primary new nodes -> all differing nodes in the new CFG are reachable from these
*)

}

type changed_global = {

old : Cil.global;
current : Cil.global;
unchangedHeader : bool;
diff : nodes_diff option;

}

type change_info = {

mutable changed : changed_global list;
mutable unchanged : Cil.global list;
mutable removed : Cil.global list;
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