--- layout: fc_discuss_archives title: Message 4 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,

> ?* 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;

Well, I would have hoped that the C99 standard would define it, but
it is very unsatisfactory in this respect (page 46, 6.3.2.1). The best
"explanation" is footnote 53:

"The name ??lvalue?? comes originally from the assignment expression
E1 = E2, in which the left
operand E1 is required to be a (modi?able) lvalue. It is perhaps
better considered as representing an
object ??locator value??. Whatis sometimes called ??rvalue?? is in
this International Standard described
as the ??value of an expression??."

Here is the foonote that I added to the value analysis manual
following your remark :

An l-value is a C expression that exists in memory.
Examples of l-values are a simple variable {\tt x}, the cell of an
array {\tt t[i]}, or a pointed location {\tt *p}. Because an l-value
lies in memory, it may have uninitialized contents. Using an
l-value when it has not yet been initialized is a forbidden
behavior that compilers do not detect in all cases, and this
is only one of the numerous pitfalls of C.

> ?* [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;

I do not use this feature myself, but I hear it gets better and better with
each Frama-C release (up to Carbon). There is also a plug-in for
distributing the functions into "services", which produce good results and
make the call graph easier to follow.

> ?* 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;

My work here is done. :)

Pascal