Frama_c_kernel.Ast_diffCompute diff information from an existing project.
module Orig_project : State_builder.Option_ref with type data = Project.tthe original project from which a diff is computed.
type 'a correspondence = [ | `Same of 'asymbol with identical definition has been found.
*)| `Not_presentno correspondence
*) ]possible correspondences between new items and original ones.
type partial_correspondence = [ | `Spec_changedbody and callees haven't changed
*)| `Body_changedspec hasn't changed
*)| `Callees_changedspec and body haven't changed
*)| `Callees_spec_changedbody hasn't changed
*) ]for kernel function, we are a bit more precise than a yes/no answer. More precisely, we check whether a function has the same spec, the same body, and whether its callees have changed (provided the body itself is identical, otherwise, there's no point in checking the callees.
module type Correspondence_table = sig ... endmodule Varinfo :
Correspondence_table
with type key = Cil_types.varinfo
and type data = Cil_types.varinfo correspondencevarinfos correspondences
module Compinfo :
Correspondence_table
with type key = Cil_types.compinfo
and type data = Cil_types.compinfo correspondencemodule Enuminfo :
Correspondence_table
with type key = Cil_types.enuminfo
and type data = Cil_types.enuminfo correspondencemodule Enumitem :
Correspondence_table
with type key = Cil_types.enumitem
and type data = Cil_types.enumitem correspondencemodule Typeinfo :
Correspondence_table
with type key = Cil_types.typeinfo
and type data = Cil_types.typeinfo correspondencemodule Stmt :
Correspondence_table
with type key = Cil_types.stmt
and type data = Cil_types.stmt code_correspondencemodule Logic_info :
Correspondence_table
with type key = Cil_types.logic_info
and type data = Cil_types.logic_info correspondencemodule Logic_type_info :
Correspondence_table
with type key = Cil_types.logic_type_info
and type data = Cil_types.logic_type_info correspondencemodule Logic_ctor_info :
Correspondence_table
with type key = Cil_types.logic_ctor_info
and type data = Cil_types.logic_ctor_info correspondencemodule Fieldinfo :
Correspondence_table
with type key = Cil_types.fieldinfo
and type data = Cil_types.fieldinfo correspondencemodule Model_info :
Correspondence_table
with type key = Cil_types.model_info
and type data = Cil_types.model_info correspondencemodule Logic_var :
Correspondence_table
with type key = Cil_types.logic_var
and type data = Cil_types.logic_var correspondencemodule Kernel_function :
Correspondence_table
with type key = Cil_types.kernel_function
and type data = Cil_types.kernel_function code_correspondencemodule Fundec :
Correspondence_table
with type key = Cil_types.fundec
and type data = Cil_types.fundec correspondenceperforms a comparison of AST between the current and the original project, which must have been set beforehand.
val compare_from_prj : Project.t -> unitcompare_from_prj prj sets prj as the original project and fill the tables.