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

[Frama-c-discuss] [Jessie] Issue with behavior in contracts




04.03.09, 14:49, "Claude March?" <Claude.Marche at inria.fr>:

> David MENTRE wrote:
> > Hello,
> > 
> > On Tue, Mar 3, 2009 at 17:30, David MENTRE <dmentre at linux-france.org> wrote:
> >> I would like to define the behaviour of read() syscall. I'm using the
> >> following contract:
> >> /*@ requires fd >= 0;
> >>    requires count > 0;
> >>    requires \valid((char*)buf+(0..count-1));
> >>    behavior error:
> >>      assigns global_error_number;
> >>      ensures \result < 0;
> >>    behavior end_of_file:
> >>      assigns \nothing;
> >>      ensures \result == 0;
> >>    behavior normal:
> >>      assigns ((char*)buf)[0..count-1];
> >>      ensures ((char*)buf)[0] >= 0 && ((char*)buf)[0] < 256;
> >>      ensures \result > 0;
> >>  */
> Even worse: since you have no assumes clauses in your behaviors, then 
> your specification says that at return, the \result is both < 0, == 0 
> and >0. This is clearly wrong


Hello.

I wanted to share some of my thoughts about this. I was also confused by behaviour in the past btw, it's not very suitable word for case separation, "case" would be more familar to C developer. And the more confusing thing is --jessie-behaviour option that from the first point of view allows to analyze some orthogonal aspect of specification without touching others.

For example

 behaviour memory:
    requires valid(a);    
 behariour safety
    requires a[0] > 1;

So that during analysis you only need to prove the obligations that work with memory or only safety statements. Now I suspect it doesn't work this way. But it would be nice to have something like that.