--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on January 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] annotations and value analysis



>  I guess it will be same with output parameters of the function  
> (gest_index(int cmd, int* pindex). Can you confirm ?

If you mean adding respectively:

   @ ensures  *p >= 10 ;
...
int get_index(int /* in */ cmd, int *p)
...
   get_index(x, &R);

It is already supported:

[value] Values for function main:
           R ? [10..199]


> And what about annotation on declaration of the function without  
> definition?

In this case you *need* an assigns clause in the function contract.
You can use dependencies (\from ...), the extension described at
page 56 of the currently distributed ACSL documentation.

The assigns clause with dependencies is interpreted
by the value analysis, but at this time, the pre- and
post-conditions are not.

The policy is that announcement of features and dates is not
allowed on this mailing-list
(as per http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-November/000780.html 
  )
and therefore, since I would never go against one of
this mailing list's official policy,
I can't have promised support for \result soon.
Similarly I can't comment on the availability of support for
pre- and post-conditions in library function specifications
in the value analysis.

Pascal

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? enlev?e...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100121/fc498cd6/attachment.htm