--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Best approach when specifying regular C functions from stdlib?



Hello,

Le lun 02 mar 2009 17:27:47 CET,
David MENTRE <dmentre at linux-france.org> a ?crit :

> 
> >> First of all, what does exactly mean "No code for function xxxxxx,
> >> default assigns generated"?
> >
> > You can look at ACSL manual, section 2.3.5. The point is that since a
> > function like read() has no code given, nor contract, then it could be
> > possible that it modifies every location in the heap. So it should be
> > given a contract.
> 
> Thank you for the precise reference to ACSL manual. I'll look at it.
> Maybe this should be given in the error message?
> 

To be completely clear, the warning says that Frama-C's kernel is
generating an assigns clause based on the function prototype, because
supposing that every location in the heap might be changed by a
function call would prevent the analyses saying something useful. The
issue is that this generated clause is not guaranteed to be correct.
For instance, given the prototype void f(int* x,int l), there's no way
to know if x is a pointer to a single int (which could be assigned l
for instance), or to a block of several ints (whose length could be l
for instance). It is thus important to review the generated clauses
(e.g. with the -print option. They are also visible in the GUI), or
better to give an appropriate contract to each prototype which has no
associated definition.

-- 
E tutto per oggi, a la prossima volta.
Virgile