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

[Frama-c-discuss] New release of Aorai



Dear Frama-C users,

A new version of the Aorai plug-in is available. It can be downloaded at :

     http://amazones.gforge.inria.fr/aorai/aorai.tgz

For timing reasons, the version includes in the Boron release is not the last
one. In the newer version, I tried to consider the two most important request,
that are :

1) When a statement is not reachable by any transition, then a warning message
   is displayed. Indeed, it correspond either to a dead code or to a statement
   that implies a property violation if reached.

2) In both Promela and YA property description languages, man can now speak
   about value of a param or of returned value. Concretely, the term f().i in a
   property characterizes the value of i parameter during the call of function
   f, while f().return characterizes the resulting value of the f function
   during its return.

   The example 'example.c' and its property 'example.ya' proposed in the example
   package are up to date with respect to this syntax:

       http://amazones.gforge.inria.fr/aorai/aorai-example.tgz

I think that these improvements correspond to the main expressed needs.

For more information, please contact me.

Best regards,
Nicolas Stouls.

-- 
====================       Nicolas Stouls      ====================
Enseignant chercheur (INSA de Lyon / ?quipe INRIA AMAZONES)
Laboratoire CITI, 6 avenue des Arts, 69621 Villeurbanne CEDEX
tel : (+33)4 72 43 73 21  | nicolas.stouls at insa-lyon.fr
fax : (+33)4 72 43 62 27  | http://perso.citi.insa-lyon.fr/nstouls/


-------------- section suivante --------------
Une pi?ce jointe autre que texte a ?t? nettoy?e...
Nom: nicolas_stouls.vcf
Type: text/x-vcard
Taille: 445 octets
Desc: non disponible
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100420/433d7786/attachment.vcf>