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] math vs. bits

On Tue, Nov 12, 2013 at 4:05 PM, David Cok <dcok at grammatech.com> wrote:

> Pascal,
>
> I've been experimenting with the Value analysis plug-in.
> But what I would really like is to be able to interact with it from my own
> plug-in, asking for and reporting the value set for specific program
> variables. Is this possible?


To read from Value's results, several options are available:

- To read a superset of possible values for an lvalue just before a
specific statement, or just after a specific statement, after the analysis
of the whole program has completed, valid for all (defined) concrete
executions that reach the statement

- To read a superset of possible values for an lvalue just before a
specific statement, or just after a specific statement, for a specific
call-stack, after the analysis of the whole program has completed, valid
for all (defined) concrete executions that reach the statement

- To read supersets of possible values while the analysis is ongoing, by
means of ?hooks?. ?Hook functions?, that is, OCaml functions written by the
user, have been registered before the analysis and the value analysis
plug-in calls them at appropriate times. Any similarity with the
customization system for a popular text editor is not fortuitous at all:
http://www.gnu.org/software/emacs/manual/html_node/emacs/Hooks.html


Any transfer of information in the other direction, that is, a user plugin
providing information it has to the value analysis plugin, can only be done
in the following three ways:

- By inserting the information beforehand in the same Abstract Syntax Tree,
as ACSL assertions

- By building a new AST from the original AST, with strategically placed
assignments, for instance x = Frama_C_interval(5, 12); in the place where
you wish to communicate that x should be assumed to lie between 5 and 12.

- By registering a hook function to do this while the analysis is ongoing,
with the caveat that:
 * either it already is possible with one of the many hooks available to
customize the value analysis, but is not documented
 * or it is possible and documented and the documentation warns about the
perils of using the hook this way
 * or it is not possible at this time, and adding the hook would be
comparatively little work, but using it safely would still be far from a
given


> Do you have any sample code that would get me started?
>

A good source of information used to be existing plugins. Values are for
instance used by the plugin From (in src/from), and also directly by the
plugin PDG, in src/pdg (in addition to the latter using results from From).
All plug-ins seem to have had a featuritis crisis, so that looking at the
Frama-C sources now, I do not see any that I would like to be recommended
to me if I was in your position.

An existing external plugin that relies on the value analysis plugin's
result is SIDAN. There may be some inspiration to get there:
http://www.rennes.supelec.fr/ren/rd/cidre/tools/sidan/down.html
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131112/a5ec3ad4/attachment-0001.html>