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:=

  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

• 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