Changelog_detailed.md

This file provides a detailed description of the main changes in the API
of Frama-C. It is intended for developers only. For a summary of all changes,
please refer to Changelog.

* Changes between Sodium and Magnesium
** Use of Value-based plug-ins:
  In case your plug-in programmatically uses one of the following plug-ins
  (even through Db):

    Value, Metrics, Occurrence, From, Users, Constant_Propagation, Inout,
    Impact, Pdg, Scope, Sparecode, Slicing

  You must add the following line in your plug-in Makefile:

  PLUGIN_DEPENDENCIES:=<plug-ins list>

  For instance, if you depend on Value, Pdg and Slicing, you must write:

  PLUGIN_DEPENDENCIES:=Value Pdg Slicing

** Callgraph Access
  In Sodium, there were three different callgraph implementations:
  - module Callgraph
  - plug-in Syntactic_callgraph (based on Callgraph)
  - plug-in Semantic_callgraph (based on Value to solve function pointers)
  The first one was almost an internal Frama-C module and directly exposed its 
  internal datastructure based on Hashtbl, while the second and the third one 
  exported a few functions through module Db.

  In Magnesium, these three modules and plug-ins are replaced by a single
  plug-in: Callgraph. This plug-in exports an API for plug-in developers through
  its interface Callgraph.mli (which is nowadays the recommended way, see
  Plug-in Development Guide, Section 3.4). The script sodium2magnesium.sh
  automatically converts the uses of Db.Syntactic_callgraph and
  Db.Semantic_callgraph to the new API, but you have to add the following line
  to your plug-in Makefile to get an access to the API:

  PLUGIN_DEPENDENCIES:=Callgraph <possibly other dependencies>

* Changes between Oxygen and Fluorine
** Removal of rooted_code_annotation
  The datatype Cil_types.rooted_code_annotation has been removed. It was used to
  distinguish between annotations present in the original sources and
  annotations generated by the plug-ins, and has never been really used.
  All functions that were using Cil_types.rooted_code_annotation now use
  directly Cil_types.code_annotation.
*** Removed identifiers
  - Constructors Cil_types.User and Cil_types.AI
  - Function Ast_info.is_trivial_rooted_assertion
    (replaced by Ast_info.is_trivial_annotation)
  - Function Ast_info.lift_annot_func (useless)
  - Function Ast_info.lift_annot_list_func (useless)
  - Function Ast_info.d_rooted_code_annotation (useless)
  - Function Annotation.code_annotation_of_rooted (useless)
  - Module Cil_datatype.Rooted_code_annotation (useless)
  - Method vrooted_code_annotation in Visitor.frama_c_visitor (useless)
*** Distinction between user annotations and generated annotations
The origin of an annotation is now given by its emitter, which can be retrieved
via Annotations.fold_code_annot and Annotations.iter_code_annot. For instance,
the following Oxygen code
#+BEGIN_SRC ocaml
Annotations.iter_code_annot
  (fun _ annot ->
    match annot with
      | User a -> f a
      | AI(_,a) -> g a)
  stmt
#+END_SRC
will be translated that way for Fluorine:
#+BEGIN_SRC ocaml
Annotations.iter_code_annot
  (fun e annot ->
     if Emitter.equal e Emitter.end_user then
       f annot
     else
       g annot)
   stmt
#+END_SRC
*** Visitor
  vrooted_code_annotation could return a list of annotations,
  while vcode_annotation must return a single annotation (however, if it is
  trivial, i.e. assert \true, it will be discarded). Code visiting 
  vrooted_code_annotation and returning several annotations at once must thus
  be rewritten (e.g. by taking care of registering the additional annotations
  directly).

** Message categories
Debug keys is a feature added in Nitrogen to allow showing only specific debug
messages of a plug-in or the kernel. Related interface has changed in Fluorine.
See src/kernel/log.mli for more details.
*** Keys for feedback and result
keys are not restricted to debug, but can be used for feedback and result.
*** New datatype
Keys were plain strings. There is now a category type, which is a private
alias for string: each key must be registered before being used.
*** Sub-categories
There are subcategories, which are implicitly defined by using columns (':')
in the category name. For instance a:b:c denotes a sub-category c of b, itself
a subcategory of a. a and a:b do not need to be already registered before
registration of a:b:c. Enabling display of messages of a will also enable
a:b and a:b:c
*** New command line options
The option for enforcing a category of message was -plugin-debug-category.
It is now -plugin-msg-key. -plugin-msg-key-unset allows to remove some
previously enabled category (either directly or as a subcategory of an enabled
category), and its subcategory. For instance 
-plugin-msg-key a -plugin-msg-unset a:b -plugin-msg-set a:b:c will enable
messages for a and a:b:c
-plugin-msg-key supports two special keys:
 - help will display the list of existing categories
 - * will enable all categories