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] Value analysis manual: questions and remarks

  • Subject: [Frama-c-discuss] Value analysis manual: questions and remarks
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Mon, 10 Jan 2011 15:18:31 +0100
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