--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on April 2010 ---
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>