--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on January 2011 ---
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