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

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.