Module `Frama_c_kernel.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.

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c.kernel/Frama_c_kernel/Ast_diff/index.html

Module `Frama_c_kernel.Ast_diff`

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c.kernel/Frama_c_kernel/Ast_diff/index.html

Module Frama_c_kernel.Ast_diff

Module `Frama_c_kernel.Ast_diff`