package goblint
Static analysis framework for C
Install
Dune Dependency
Authors
Maintainers
Sources
goblint-2.5.0.tbz
sha256=452d8491527aea21f2cbb11defcc14ba0daf9fdb6bdb9fc0af73e56eac57b916
sha512=1993cd45c4c7fe124ca6e157f07d17ec50fab5611b270a434ed1b7fb2910aa85a8e6eaaa77dad770430710aafb2f6d676c774dd33942d921f23e2f9854486551
doc/goblint.incremental/CompareCIL/index.html
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
module StringMap = CompareCFG.StringMap
Source
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 (&&>>) :
(bool * rename_mapping) ->
(rename_mapping:rename_mapping -> bool * rename_mapping) ->
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
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
Source
val mem_typ_acc :
GoblintCil.typ ->
GoblintCil.typ ->
(GoblintCil.typ * GoblintCil.typ) list ->
bool
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
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
module NH = CompareCFG.NH
Source
type 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) Stdlib.Seq.t * NH.key Stdlib.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
module FundecMap = CilMaps.FundecMap
module VarinfoMap = CilMaps.VarinfoMap
module GlobalMap : sig ... end
module GlobalColMap : sig ... end
Source
type nodes_diff = {
unchangedNodes : (MyCFG.node * MyCFG.node) list;
primObsoleteNodes : MyCFG.node list;
(*primary obsolete nodes -> all obsolete nodes are reachable from these
*)
}
For semantically unchanged globals, still keep old and current version of global for resetting current to old.
Source
type changed_global = {
old : global_col;
current : global_col;
unchangedHeader : bool;
diff : nodes_diff option;
}
module VarinfoSet : sig ... end
Source
type 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.
}
Source
type change_status =
| Unchanged
| Changed
| ChangedFunHeader of GoblintCil.Cil.fundec
| ForceReanalyze of GoblintCil.Cil.fundec
Given a boolean that indicates whether the code object is identical to the previous version, returns the corresponding change_status
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
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.global
s, an old and a new Cil.file
, this function computes a change_info
, which describes which global
s are changed, unchanged, removed and added.
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>