Frama-C API - `Ast_diff`

Compute diff information from an existing project.

since 25.0-Manganese

module Orig_project : State_builder.Option_ref with type data = Project.t

the original project from which a diff is computed.

type 'a correspondence = [

| `Same of 'a
(*
symbol with identical definition has been found.
*)
| `Not_present
(*
no correspondence
*)

]

possible correspondences between new items and original ones.

type partial_correspondence = [

| `Spec_changed
(*
body and callees haven't changed
*)
| `Body_changed
(*
spec hasn't changed
*)
| `Callees_changed
(*
spec and body haven't changed
*)
| `Callees_spec_changed
(*
body 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.

type 'a code_correspondence = [

| 'a correspondence
| `Partial of 'a * partial_correspondence

]

module type Correspondence_table = sig ... end

module Varinfo : Correspondence_table with type key = Cil_types.varinfo and type data = Cil_types.varinfo correspondence

varinfos correspondences

module Compinfo : Correspondence_table with type key = Cil_types.compinfo and type data = Cil_types.compinfo correspondence

module Enuminfo : Correspondence_table with type key = Cil_types.enuminfo and type data = Cil_types.enuminfo correspondence

module Enumitem : Correspondence_table with type key = Cil_types.enumitem and type data = Cil_types.enumitem correspondence

module Typeinfo : Correspondence_table with type key = Cil_types.typeinfo and type data = Cil_types.typeinfo correspondence

module Stmt : Correspondence_table with type key = Cil_types.stmt and type data = Cil_types.stmt code_correspondence

module Logic_info : Correspondence_table with type key = Cil_types.logic_info and type data = Cil_types.logic_info correspondence

module Logic_type_info : Correspondence_table with type key = Cil_types.logic_type_info and type data = Cil_types.logic_type_info correspondence

module Logic_ctor_info : Correspondence_table with type key = Cil_types.logic_ctor_info and type data = Cil_types.logic_ctor_info correspondence

module Fieldinfo : Correspondence_table with type key = Cil_types.fieldinfo and type data = Cil_types.fieldinfo correspondence

module Model_info : Correspondence_table with type key = Cil_types.model_info and type data = Cil_types.model_info correspondence

module Logic_var : Correspondence_table with type key = Cil_types.logic_var and type data = Cil_types.logic_var correspondence

module Kernel_function : Correspondence_table with type key = Cil_types.kernel_function and type data = Cil_types.kernel_function code_correspondence

module Fundec : Correspondence_table with type key = Cil_types.fundec and type data = Cil_types.fundec correspondence

type is_same_env

map of symbols currently under comparison, with their correspondence status so far

val is_same_list : ('a -> 'a -> is_same_env -> bool) -> 'a list -> 'a list -> is_same_env -> bool

val is_same_term : Cil_types.term -> Cil_types.term -> is_same_env -> bool

val is_same_predicate : Cil_types.predicate -> Cil_types.predicate -> is_same_env -> bool

val set_extension_diff : is_same_ext: (plugin:string -> string -> Cil_types.acsl_extension_kind -> Cil_types.acsl_extension_kind -> is_same_env -> bool) -> unit

alert acsl_extension_handler This function can only be called by Acsl_extension

val compare_ast : unit -> unit

performs a comparison of AST between the current and the original project, which must have been set beforehand.

val compare_from_prj : Project.t -> unit

compare_from_prj prj sets prj as the original project and fill the tables.

Frama-C API - Ast_diff

Frama-C API - `Ast_diff`