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: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Mon, 10 Jan 2011 15:58:15 +0100
  • In-reply-to: <AANLkTi=AOF2nkFeK8SUWNBFCdDzi8WMoOBE34GSmyo8Q@mail.gmail.com>
  • References: <AANLkTi=AOF2nkFeK8SUWNBFCdDzi8WMoOBE34GSmyo8Q@mail.gmail.com>
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