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

On Mon, Mar 2, 2009 at 17:09, Claude March? <Claude.Marche at inria.fr> wrote:
>> and even rejects certain forms (for main():
>> "Bug: unsupported variadic functions").
>
> I'm not sure about this one: does it happen if you use int main(int
> argc, char *argv[]) ?

Just tested: yes, same issue.

Maybe the error reporting in unprecise and the faulty line is not the
reported one? The used source code is:
  http://www.linux-france.org/~dmentre/code/dev-random-pass-gen.c

In above code, I've just replaced the printf() by putchar()s.

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

> I recommend not to modify regular system headers. You can simply augment
> your source code with contracts for functions you use (or put them in a
> separate file that you #include). e.g
>
> /*@ requires \valid(buf+(0..count-1));
> ? @ assigns errno, buf[0..count-1];
> ? @*/
> ssize_t read(int fd, void *buf, size_t count);

Ok, I'll do that. Of course, in the meantime I've chosen the reverse path. ;-)

> In principle, Frama-C should be shipped with contracts for standard
> library functions, but this is not an easy thing to do: it is not clear
> at all what would be a "universal" contract for all use of thos functions...

I understand. And I assume refining contracts for a specific
environment might help proving properties.

Many thanks for your help,
Yours,
d.