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. S
    Simmo Saan
  2. M
    Michael Schwarz
  3. J
    Julian Erhard
  4. S
    Sarah Tilscher
  5. R
    Ralf Vogler
  6. K
    Kalmer Apinis
  7. V
    Vesal Vojdani

Maintainers

  1. S
    Simmo Saan <simmo.saan@gmail.com>
  2. M
    Michael Schwarz <michael.schwarz93@gmail.com>

Sources

goblint-2.3.0.tbz
sha256=b729c94adb383a39aea32eb005c988dfd44b92af22ee6a4eedf4239542ac6c26
sha512=643b98770e5fe5644324c95c9ae3a9f698f25c8b11b298f0751d524e0b20af368b2a465fc8200b75a73d48fc9a053fd90f5e8920d4db070927f93188bb8687e0

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

Module Goblint_lib.CompareCIL

Comparison of CIL files.

include module type of struct include CompareAST end
include module type of struct include CompareCFG end
include module type of struct include CompareAST end
module StringMap = CompareAST.StringMap
type method_rename_assumptions = GoblintCil.varinfo CilMaps.VarinfoMap.t
type glob_var_rename_assumptions = GoblintCil.varinfo CilMaps.VarinfoMap.t
type renamesOnSuccess = (GoblintCil.compinfo * GoblintCil.compinfo) list * (GoblintCil.enuminfo * GoblintCil.enuminfo) list
val rename_mapping_aware_name_comparison : string -> string -> rename_mapping -> bool
val create_locals_rename_mapping : string list -> string list -> string StringMap.t
val is_rename_mapping_empty : rename_mapping -> bool
val (&&>>) : (bool * rename_mapping) -> (rename_mapping:rename_mapping -> bool * rename_mapping) -> bool * rename_mapping
val (&&>) : (bool * rename_mapping) -> bool -> bool * rename_mapping
val forward_list_equal : ?propF: ((bool * rename_mapping) -> (rename_mapping:rename_mapping -> bool * rename_mapping) -> bool * rename_mapping) -> ('a -> 'b -> rename_mapping:rename_mapping -> bool * rename_mapping) -> 'a list -> 'b list -> rename_mapping:rename_mapping -> bool * rename_mapping
val compare_name : string -> string -> bool
val eq_constant : rename_mapping:rename_mapping -> acc:(GoblintCil.typ * GoblintCil.typ) list -> GoblintCil.constant -> GoblintCil.constant -> bool * rename_mapping
val eq_lhost : GoblintCil.lhost -> GoblintCil.lhost -> rename_mapping:rename_mapping -> acc:(GoblintCil.typ * GoblintCil.typ) list -> bool * rename_mapping
val global_typ_acc : (GoblintCil.typ * GoblintCil.typ) list ref
val mem_typ_acc : GoblintCil.typ -> GoblintCil.typ -> (GoblintCil.typ * GoblintCil.typ) list -> bool
val pretty_length : unit -> (GoblintCil.typ * GoblintCil.typ) list -> GoblintCil.Pretty.doc
val eq_typ_acc : ?fun_parameter_name_comparison_enabled:bool -> GoblintCil.typ -> GoblintCil.typ -> rename_mapping:rename_mapping -> acc:(GoblintCil.typ * GoblintCil.typ) list -> bool * rename_mapping
val eq_eitems : (string * GoblintCil.exp * GoblintCil.location) -> (string * GoblintCil.exp * GoblintCil.location) -> rename_mapping:rename_mapping -> acc:(GoblintCil.typ * GoblintCil.typ) list -> bool * rename_mapping
val eq_enuminfo : GoblintCil.enuminfo -> GoblintCil.enuminfo -> rename_mapping:rename_mapping -> acc:(GoblintCil.typ * GoblintCil.typ) list -> bool * rename_mapping
val eq_args : ?fun_parameter_name_comparison_enabled:bool -> (string * GoblintCil.typ * GoblintCil.attributes) -> (string * GoblintCil.typ * GoblintCil.attributes) -> rename_mapping:rename_mapping -> acc:(GoblintCil.typ * GoblintCil.typ) list -> bool * rename_mapping
val eq_attrparam : GoblintCil.attrparam -> GoblintCil.attrparam -> rename_mapping:rename_mapping -> acc:(GoblintCil.typ * GoblintCil.typ) list -> bool * rename_mapping
val eq_attribute : GoblintCil.attribute -> GoblintCil.attribute -> acc:(GoblintCil.typ * GoblintCil.typ) list -> rename_mapping:rename_mapping -> bool * rename_mapping
val eq_compinfo : GoblintCil.compinfo -> GoblintCil.compinfo -> (GoblintCil.typ * GoblintCil.typ) list -> rename_mapping -> bool * rename_mapping
val eq_fieldinfo : GoblintCil.fieldinfo -> GoblintCil.fieldinfo -> acc:(GoblintCil.typ * GoblintCil.typ) list -> rename_mapping:rename_mapping -> bool * rename_mapping
val eq_typ : ?fun_parameter_name_comparison_enabled:bool -> GoblintCil.typ -> GoblintCil.typ -> rename_mapping:rename_mapping -> bool * rename_mapping
val eq_exp : GoblintCil.exp -> GoblintCil.exp -> rename_mapping:rename_mapping -> bool * rename_mapping
val eq_varinfo : GoblintCil.varinfo -> GoblintCil.varinfo -> rename_mapping:rename_mapping -> bool * rename_mapping
val eq_lval : GoblintCil.lval -> GoblintCil.lval -> rename_mapping:rename_mapping -> bool * rename_mapping
val eq_offset : GoblintCil.offset -> GoblintCil.offset -> rename_mapping:rename_mapping -> bool * rename_mapping
val eq_instr : GoblintCil.instr -> GoblintCil.instr -> rename_mapping:rename_mapping -> bool * rename_mapping
val eq_label : GoblintCil.label -> GoblintCil.label -> bool
val eq_stmt_with_location : (GoblintCil.stmt * GoblintCil.fundec) -> (GoblintCil.stmt * GoblintCil.fundec) -> bool
val eq_stmtkind : ?cfg_comp:bool -> (GoblintCil.stmtkind * GoblintCil.fundec) -> (GoblintCil.stmtkind * GoblintCil.fundec) -> rename_mapping:rename_mapping -> bool * rename_mapping
val eq_stmt : ?cfg_comp:bool -> (GoblintCil.stmt * GoblintCil.fundec) -> (GoblintCil.stmt * GoblintCil.fundec) -> rename_mapping:rename_mapping -> bool * rename_mapping
val eq_block : (GoblintCil.Cil.block * GoblintCil.fundec) -> (GoblintCil.Cil.block * GoblintCil.fundec) -> rename_mapping:rename_mapping -> bool * rename_mapping
val eq_init : GoblintCil.init -> GoblintCil.init -> rename_mapping:rename_mapping -> bool * rename_mapping
val eq_initinfo : GoblintCil.initinfo -> GoblintCil.initinfo -> rename_mapping:rename_mapping -> bool * rename_mapping
val (&&<>) : (bool * rename_mapping) -> (rename_mapping:rename_mapping -> bool * rename_mapping) -> bool * rename_mapping
val eq_node : (MyCFG.node * GoblintCil.fundec) -> (MyCFG.node * GoblintCil.fundec) -> rename_mapping:rename_mapping -> bool * rename_mapping
val eq_edge : MyCFG.edge -> MyCFG.edge -> rename_mapping:rename_mapping -> bool * rename_mapping
val eq_edge_list : MyCFG.edge list -> MyCFG.edge list -> rename_mapping:rename_mapping -> bool * rename_mapping
val to_edge_list : ('a * 'b) list -> 'b list
module NH = CompareCFG.NH
type biDirectionNodeMap = CompareCFG.biDirectionNodeMap = {
  1. node1to2 : MyCFG.node NH.t;
  2. node2to1 : MyCFG.node NH.t;
}
val compareCfgs : (module MyCFG.CfgForward) -> (module MyCFG.CfgForward) -> GoblintCil.fundec -> GoblintCil.fundec -> rename_mapping -> biDirectionNodeMap * unit NH.t * rename_mapping
val reexamine : 'a -> CilType.Fundec.t -> biDirectionNodeMap -> unit NH.t -> (module MyCFG.CfgForward) -> (module MyCFG.CfgBidir) -> (NH.key * MyCFG.node) Seq.t * NH.key Seq.t
val compareFun : (module MyCFG.CfgForward) -> (module MyCFG.CfgBidir) -> GoblintCil.fundec -> GoblintCil.fundec -> rename_mapping -> (MyCFG.node * MyCFG.node) list * MyCFG.node list * rename_mapping
include module type of struct include CilMaps end
module FundecForMap = CilMaps.FundecForMap
module FundecMap = CilMaps.FundecMap
module VarinfoOrdered = CilMaps.VarinfoOrdered
module VarinfoMap = CilMaps.VarinfoMap
module GlobalMap : sig ... end
type global_def =
  1. | Var of GoblintCil.varinfo
  2. | Fun of GoblintCil.fundec
type global_col = {
  1. decls : GoblintCil.varinfo option;
  2. def : global_def option;
}
val name_of_global_col : global_col -> string
val compare_global_col : global_col -> global_col -> int
val equal_name_global_col : global_col -> global_col -> bool
val get_varinfo : global_col -> GoblintCil.varinfo
module GlobalColMap : sig ... end
val name_of_global : GoblintCil.global -> string
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

    *)
}
type unchanged_global = {
  1. old : global_col;
  2. current : global_col;
}

For semantically unchanged globals, still keep old and current version of global for resetting current to old.

type changed_global = {
  1. old : global_col;
  2. current : global_col;
  3. unchangedHeader : bool;
  4. diff : nodes_diff option;
}
module VarinfoSet : sig ... end
type change_info = {
  1. mutable changed : changed_global list;
  2. mutable unchanged : unchanged_global list;
  3. mutable removed : global_col list;
  4. mutable added : global_col list;
  5. mutable exclude_from_rel_destab : VarinfoSet.t;
    (*

    Set of functions that are to be force-reanalyzed. These functions are additionally included in the changed field, among the other changed globals.

    *)
}
val empty_change_info : unit -> change_info
type change_status =
  1. | Unchanged
  2. | Changed
  3. | ChangedFunHeader of GoblintCil.Cil.fundec
  4. | ForceReanalyze of GoblintCil.Cil.fundec
val unchanged_to_change_status : bool -> change_status

Given a boolean that indicates whether the code object is identical to the previous version, returns the corresponding change_status

val empty_rename_mapping : rename_mapping
val should_reanalyze : GoblintCil.Cil.fundec -> bool
val performRenames : renamesOnSuccess -> unit
val preservesSameNameMatches : GlobalMap.key -> 'a GlobalMap.t -> GlobalMap.key -> 'b GlobalMap.t -> bool
val empty_rename_assms : GoblintCil.varinfo VarinfoMap.t -> bool
val already_matched : VarinfoMap.key -> 'a -> (GoblintCil.varinfo VarinfoMap.t * 'b) -> bool
val change_info_lookup : global_col -> global_col -> change_info -> bool
val eq_glob_var : ?finalizeOnlyExactMatch:bool -> VarinfoMap.key -> global_col -> 'a GlobalMap.t -> GoblintCil.varinfo -> global_col -> 'b GlobalMap.t -> change_info -> (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t) -> bool * change_info * (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t)
val eqF_check_contained_renames : renameDetection:bool -> GoblintCil.Cil.fundec -> GoblintCil.Cil.fundec -> global_col GlobalMap.t -> global_col GlobalMap.t -> (MyCFG.cfg * (MyCFG.cfg * MyCFG.cfg)) option -> global_col -> global_col -> (change_info * (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t)) -> change_info * (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t)
val addNewGlobals : 'a -> global_col -> (change_info * ('b * 'c VarinfoMap.t)) -> change_info * ('b * 'c VarinfoMap.t)
val addOldGlobals : 'a -> global_col -> (change_info * ('b VarinfoMap.t * 'c)) -> change_info * ('b VarinfoMap.t * 'c)
val compareCilFiles : ?eq: (?matchVars:bool -> ?matchFuns:bool -> ?renameDetection:bool -> global_col GlobalMap.t -> global_col GlobalMap.t -> (MyCFG.cfg * (MyCFG.cfg * MyCFG.cfg)) option -> global_col -> global_col -> (change_info * (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t)) -> change_info * (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t)) -> GoblintCil.file -> GoblintCil.file -> change_info

Given an (optional) equality function between Cil.globals, an old and a new Cil.file, this function computes a change_info, which describes which globals are changed, unchanged, removed and added.