Module `CompareCIL`Source

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

Sourcemodule StringMap = CompareCFG.StringMap

Sourcetype method_rename_assumptions = GoblintCil.varinfo CilMaps.VarinfoMap.t

Sourcetype glob_var_rename_assumptions = GoblintCil.varinfo CilMaps.VarinfoMap.t

type renamesOnSuccess =
  (GoblintCil.compinfo * GoblintCil.compinfo) list
  * (GoblintCil.enuminfo * GoblintCil.enuminfo) list

Source

type rename_mapping =
  string StringMap.t
  * method_rename_assumptions
  * glob_var_rename_assumptions
  * renamesOnSuccess

Source

val rename_mapping_aware_name_comparison : 
  string ->
  string ->
  rename_mapping ->
  bool

Source

val create_locals_rename_mapping : 
  string list ->
  string list ->
  string StringMap.t

Sourceval is_rename_mapping_empty : rename_mapping -> bool

Source

val (&&>>) : 
  (bool * rename_mapping) ->
  (rename_mapping:rename_mapping -> bool * rename_mapping) ->
  bool * rename_mapping

Sourceval (&&>) : (bool * rename_mapping) -> bool -> bool * rename_mapping

Source

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

Sourceval compare_name : string -> string -> bool

Source

val eq_constant : 
  rename_mapping:rename_mapping ->
  acc:(GoblintCil.typ * GoblintCil.typ) list ->
  GoblintCil.constant ->
  GoblintCil.constant ->
  bool * rename_mapping

Source

val eq_lhost : 
  GoblintCil.lhost ->
  GoblintCil.lhost ->
  rename_mapping:rename_mapping ->
  acc:(GoblintCil.typ * GoblintCil.typ) list ->
  bool * rename_mapping

Sourceval global_typ_acc : (GoblintCil.typ * GoblintCil.typ) list ref

Source

val mem_typ_acc : 
  GoblintCil.typ ->
  GoblintCil.typ ->
  (GoblintCil.typ * GoblintCil.typ) list ->
  bool

Source

val pretty_length : 
  unit ->
  (GoblintCil.typ * GoblintCil.typ) list ->
  GoblintCil.Pretty.doc

Source

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

Source

val eq_eitems : 
  (string * GoblintCil.attributes * GoblintCil.exp * GoblintCil.location) ->
  (string * GoblintCil.attributes * GoblintCil.exp * GoblintCil.location) ->
  rename_mapping:rename_mapping ->
  acc:(GoblintCil.typ * GoblintCil.typ) list ->
  bool * rename_mapping

Source

val eq_enuminfo : 
  GoblintCil.enuminfo ->
  GoblintCil.enuminfo ->
  rename_mapping:rename_mapping ->
  acc:(GoblintCil.typ * GoblintCil.typ) list ->
  bool * rename_mapping

Source

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

Source

val eq_attrparam : 
  GoblintCil.attrparam ->
  GoblintCil.attrparam ->
  rename_mapping:rename_mapping ->
  acc:(GoblintCil.typ * GoblintCil.typ) list ->
  bool * rename_mapping

Source

val eq_attribute : 
  GoblintCil.attribute ->
  GoblintCil.attribute ->
  acc:(GoblintCil.typ * GoblintCil.typ) list ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_compinfo : 
  GoblintCil.compinfo ->
  GoblintCil.compinfo ->
  (GoblintCil.typ * GoblintCil.typ) list ->
  rename_mapping ->
  bool * rename_mapping

Source

val eq_fieldinfo : 
  GoblintCil.fieldinfo ->
  GoblintCil.fieldinfo ->
  acc:(GoblintCil.typ * GoblintCil.typ) list ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_typ : 
  ?fun_parameter_name_comparison_enabled:bool ->
  GoblintCil.typ ->
  GoblintCil.typ ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_exp : 
  GoblintCil.exp ->
  GoblintCil.exp ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_varinfo : 
  GoblintCil.varinfo ->
  GoblintCil.varinfo ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_lval : 
  GoblintCil.lval ->
  GoblintCil.lval ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_offset : 
  GoblintCil.offset ->
  GoblintCil.offset ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_instr : 
  GoblintCil.instr ->
  GoblintCil.instr ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Sourceval eq_label : GoblintCil.label -> GoblintCil.label -> bool

Source

val eq_stmt_with_location : 
  (GoblintCil.stmt * GoblintCil.fundec) ->
  (GoblintCil.stmt * GoblintCil.fundec) ->
  bool

Source

val eq_stmtkind : 
  ?cfg_comp:bool ->
  (GoblintCil.stmtkind * GoblintCil.fundec) ->
  (GoblintCil.stmtkind * GoblintCil.fundec) ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_stmt : 
  ?cfg_comp:bool ->
  (GoblintCil.stmt * GoblintCil.fundec) ->
  (GoblintCil.stmt * GoblintCil.fundec) ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_block : 
  (GoblintCil.Cil.block * GoblintCil.fundec) ->
  (GoblintCil.Cil.block * GoblintCil.fundec) ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_init : 
  GoblintCil.init ->
  GoblintCil.init ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_initinfo : 
  GoblintCil.initinfo ->
  GoblintCil.initinfo ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val (&&<>) : 
  (bool * rename_mapping) ->
  (rename_mapping:rename_mapping -> bool * rename_mapping) ->
  bool * rename_mapping

Source

val eq_node : 
  (MyCFG.node * GoblintCil.fundec) ->
  (MyCFG.node * GoblintCil.fundec) ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_edge : 
  MyCFG.edge ->
  MyCFG.edge ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_edge_list : 
  MyCFG.edge list ->
  MyCFG.edge list ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Sourceval to_edge_list : ('a * 'b) list -> 'b list

Sourcemodule NH = CompareCFG.NH

Sourcetype biDirectionNodeMap = CompareCFG.biDirectionNodeMap = {

node1to2 : MyCFG.node NH.t;
node2to1 : MyCFG.node NH.t;

}

Source

val compareCfgs : 
  (module MyCFG.CfgForward) ->
  (module MyCFG.CfgForward) ->
  GoblintCil.fundec ->
  GoblintCil.fundec ->
  rename_mapping ->
  biDirectionNodeMap * unit NH.t * rename_mapping

Source

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

Source

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

Sourcemodule FundecForMap = CilMaps.FundecForMap

Sourcemodule FundecMap = CilMaps.FundecMap

Sourcemodule VarinfoOrdered = CilMaps.VarinfoOrdered

Sourcemodule VarinfoMap = CilMaps.VarinfoMap

Sourcemodule GlobalMap : sig ... end

Sourcetype global_def =

| Var of GoblintCil.varinfo
| Fun of GoblintCil.fundec

Sourcetype global_col = {

decls : GoblintCil.varinfo option;
def : global_def option;

}

Sourceval name_of_global_col : global_col -> string

Sourceval compare_global_col : global_col -> global_col -> int

Sourceval equal_name_global_col : global_col -> global_col -> bool

Sourceval get_varinfo : global_col -> GoblintCil.varinfo

Sourcemodule GlobalColMap : sig ... end

Sourceval name_of_global : GoblintCil.global -> string

Sourcetype nodes_diff = {

unchangedNodes : (MyCFG.node * MyCFG.node) list;
primObsoleteNodes : MyCFG.node list;
(*
primary obsolete nodes -> all obsolete nodes are reachable from these
*)

}

Sourcetype unchanged_global = {

old : global_col;
current : global_col;

}

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

Sourcetype changed_global = {

old : global_col;
current : global_col;
unchangedHeader : bool;
diff : nodes_diff option;

}

Sourcemodule VarinfoSet : sig ... end

Sourcetype change_info = {

mutable changed : changed_global list;
mutable unchanged : unchanged_global list;
mutable removed : global_col list;
mutable added : global_col list;
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.
*)

}

Sourceval empty_change_info : unit -> change_info

Sourcetype change_status =

| Unchanged
| Changed
| ChangedFunHeader of GoblintCil.Cil.fundec
| ForceReanalyze of GoblintCil.Cil.fundec

Sourceval 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

Sourceval empty_rename_mapping : rename_mapping

Sourceval should_reanalyze : GoblintCil.Cil.fundec -> bool

Sourceval performRenames : renamesOnSuccess -> unit

Source

val preservesSameNameMatches : 
  GlobalMap.key ->
  'a GlobalMap.t ->
  GlobalMap.key ->
  'b GlobalMap.t ->
  bool

Source

val addToFinalMatchesMapping : 
  VarinfoMap.key ->
  VarinfoMap.key ->
  (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t) ->
  VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t

Sourceval empty_rename_assms : GoblintCil.varinfo VarinfoMap.t -> bool

Source

val already_matched : 
  VarinfoMap.key ->
  'a ->
  (GoblintCil.varinfo VarinfoMap.t * 'b) ->
  bool

Sourceval change_info_lookup : global_col -> global_col -> change_info -> bool

Source

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)

Source

val compare_varinfo_exact : 
  VarinfoMap.key ->
  global_col ->
  global_col GlobalMap.t ->
  GoblintCil.varinfo ->
  global_col ->
  global_col GlobalMap.t ->
  change_info ->
  (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t) ->
  bool
  * change_info
  * (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t)

Source

val eqF : 
  GoblintCil.Cil.fundec ->
  GoblintCil.Cil.fundec ->
  (MyCFG.cfg * (MyCFG.cfg * MyCFG.cfg)) option ->
  method_rename_assumptions ->
  glob_var_rename_assumptions ->
  change_status
  * nodes_diff option
  * method_rename_assumptions
  * glob_var_rename_assumptions
  * renamesOnSuccess

Source

val eqF_only_consider_exact_match : 
  global_col ->
  global_col ->
  change_info ->
  (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t) ->
  global_col GlobalMap.t ->
  global_col GlobalMap.t ->
  bool
  * change_info
  * (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t)

Source

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)

Source

val eq_glob : 
  ?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)

Source

val addNewGlobals : 
  'a ->
  global_col ->
  (change_info * ('b * 'c VarinfoMap.t)) ->
  change_info * ('b * 'c VarinfoMap.t)

Source

val addOldGlobals : 
  'a ->
  global_col ->
  (change_info * ('b VarinfoMap.t * 'c)) ->
  change_info * ('b VarinfoMap.t * 'c)

Source

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.

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/goblint.incremental/CompareCIL/index.html

Module `CompareCIL`Source

package goblint

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/goblint.incremental/CompareCIL/index.html

Module CompareCILSource

dune-project
Dependency

Module `CompareCIL`Source