package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Compute diff information from an existing project.

  • since 25.0-Manganese

the original project from which a diff is computed.

type 'a correspondence = [
  1. | `Same of 'a
    (*

    symbol with identical definition has been found.

    *)
  2. | `Not_present
    (*

    no correspondence

    *)
]

possible correspondences between new items and original ones.

type partial_correspondence = [
  1. | `Spec_changed
    (*

    body and callees haven't changed

    *)
  2. | `Body_changed
    (*

    spec hasn't changed

    *)
  3. | `Callees_changed
    (*

    spec and body haven't changed

    *)
  4. | `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 = [
  1. | 'a correspondence
  2. | `Partial of 'a * partial_correspondence
]
module type Correspondence_table = sig ... end

varinfos correspondences

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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct