Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Boron and the Annotations module

Hello Pierre-Lo?c,

Pierre-Lo?c Garoche a ?crit :
> could I get some information about the motivations to add the Project.Computation.t arguments to all functions in the annotations module ?

Each value of type Project.Computation.t represents a Frama-C state. A 
state gets one different mutable value by project while the 
corresponding value of type Project.Computation.t is not project 
dependent and is immutable. There are hundreds of states in Frama-C. The 
corresponding values of type Project.Computation.t are named 
"Module_name.self" by convention. Only some of them are usable from 
outside. For instance, there is one state by command line option, one 
state for the AST (Ast.self), one other for the results of the value 
analysis plug-in (Db.Value.self) and one other for the table storing the 
code annotations (Annotations.self).

Each state may depend on other states. That is required for ensuring the 
consistency of Frama-C results. For instance, thank to these 
dependencies, if someone sets one parameter of the value analysis 
plug-in, the results of this plug-in are automatically erased, then 
re-computed according to the new value of the modified parameter. More 
details are provided Section 4.11 of the Frama-C Plug-in Development 
Guide (http://frama-c.com/download/plugin-developer-Boron-20100401.pdf).

What is new in Frama-C Boron? Frama-C Boron introduces fine-grained 
states: each code annotation (not only the whole table) is a state, 
allowing dependencies from/to single code annotations. That is reflected 
in the API of the module Annotations by the additional 
Project.Computation.t arguments. For instance, thank to them, if someone 
sets one parameter of the value analysis plug-in, the results of this 
plug-in are automatically erased (as before) **and** also the assertions 
introduced by this plug-in (but not the other code annotations).

I agree that these fine-grained states are not yet well documented. 
Please fill a feature request on the Frama-C BTS if you wish a detailed 
documentation. Actually, fine-grained states are ongoing work: they are 
only the first step for a new feature which should be part of the next 
major release hopefully...

> - What is the difference with the function "Project.on" used on the Annotations functions ?

Sorry but I don't understand which use of the function "Project.on" you 
are talking about.

> - How to get the Project.Computation value of a Project ? I only find Ast.self and Annotations.self.

In order to know which Project.Computation.t values exist, grep "self" 
in the Frama-C source (or find "self" in the index of the ocamldoc 
documentation). In Frama-C Boron, you can also run the Frama-C GUI in 
debug mode, then click on the menu entry "Debug" of the GUI, then click 
on the item "State Dependency Graph": you will see all the existing 
states with their dependencies. That is my favorite tool when I search a 
missing/incorrect dependency.

> Some hints would be welcomed.

Hope this helps,
Julien