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] 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.