Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] New release of Aorai

  • Subject: [Frama-c-discuss] New release of Aorai
  • From: nicolas.stouls at insa-lyon.fr (Nicolas Stouls)
  • Date: Tue, 20 Apr 2010 13:09:10 +0200
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>