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] a question on functional dependency analysis

  • Subject: [Frama-c-discuss] a question on functional dependency analysis
  • From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
  • Date: Fri Aug 29 13:50:19 2008
  • In-reply-to: <1220004053.798.26.camel@elfe>
  • References: <1220004053.798.26.camel@elfe>
On Aug 29, 2008, at 12:00 PM, David DELMAS wrote:

>   __fun_cpt FROM h; __fun_cpt; (and default:false)
Hi David,

we agree that there is a little fuzziness in what the analyzer does
with your "assigns" clause in this example.

Let us first look at the tools that you making use of here.
One is ACSL's "assigns" clause in a function contract. The other
is the (automatically computed from the results of the value analysis)
-deps analysis.

ACSL assigns clauses are intended to specify functional dependencies.
In this context, there is no difference between a function f that
a/ assigning a new value to variable y that happens to be computed
from the previous value of y
and
b/ possibly not assigning variable y in the function, so that it would
have retained its previous value after the function call.
Both are specified in exactly the same way: "assigns y \from y;".
The value of y after a call to f depends functionally of the value
of y before the call.

The analysis that is launched with the -deps command-line option,
on the other hand, distinguishes between a/ and b/, because it
has a notion of "possibly not having been assigned" for a variable,
which is printed as "default:true". The message "default:false" on
the other hand guarantees that the variable is assigned during
the execution of the function.

For functions for which the source code is not available, it is
desirable to use the "assigns" clauses, if present, for the
-deps analysis. For this reason, a module was written inside
Frama-C for translating
the assigns clauses into dependencies in the -deps format.
The reason the Frama-C implementers thought
it would be okay to have default:false in an example such as
yours is that if a variable, such as __fun_cpt in your example, might
not be assigned, it would appear in the "assigns" clause, and
therefore be mentioned as an explicit dependency on the
right-hand side (as it is in your example).

There is a slight problem with this approach, which I think is
the reason you are asking about this example.
Some implementations for function fun can satisfy the
assigns clause without satisfying the translation of this
clause into the -deps format. For instance, consider the following
implementation for function fun

int fun(int x)
{
   if (__fun_cpt)
     __fun_cpt++;
   return (x + fun_cpt);
}

This implementation satisfies the contract in your example.
But if the -deps analysis is launched on
this implementation of fun, the resulting dependencies contain
__fun_cpt FROM __fun_cpt (and default:true)

This may disturb you because this dependency is different
(and indeed is not included in) the dependency that was computed
from the contract when the implementation was not available.

We agree that this needs to be fixed. But was this the problem
that you had with the treatment of your example? In your
example, the "default:false" that puzzles you comes from the fact
that fun is called systematically by main2, and that the function fun
has the dependency __fun_cpt FROM __fun_cpt; (and default:false)
(this is just to evaluate the urgency of this fix, and whether
you consider your question answered).

Pascal

-------------- section suivante --------------
Une pièce jointe HTML a été enlevée...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20080829/c85e3991/attachment.htm