--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on January 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Value analysis manual: questions and remarks



Hello,

I read the value analysis manual of Frama-C Boron and I have therefore
several questions and remarks:

 * What is an l-value? I have my own idea (left part of a C
assignation) but as far as I know the term is not defined in the
manual;

 * [more a feature wish] The Call-graph displayed on a non trivial
example (ex. skein example of the manual) by a call to Analyses->Show
callgraph is unreadable (spaghetti of boxes and arrows). I think it
would be better to display it in text form with references, for
example as done by GNU cflow;

 * When doing the skein example (Tutorial, chapt. 3 of the manual), I
searched a long time on the output of program of section 3.3.1 because
I wasn't obtaining the same result, and even different results between
two executions! Until I realised in section 3.4.2 that the initial
proposed code is (intentionally) buggy. Putting a warning in section
3.3.1 would be helpful;

 * There is no explanation on the purpose of the different Frama_C_*
functions in section 8.2.1 (Adding non-determinism). In fact, they are
briefly described in the example found at the end of share/builtin.c.
A few lines of description in the manual would be helpful.

Beyond those few remarks, I found the manual well written, with very
helpful examples. Thanks a lot!

Sincerely yours,
david