--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on March 2009 ---
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.