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

[Frama-c-discuss] Syntax of negation



Hello Boris,

Le lun. 17 janv. 2011 16:49:40 CET,
Boris Hollas <hollas at informatik.htw-dresden.de> a ?crit :

> According to 2.2.1 Operators precedence in the ACSL manual, the
> expression
> 
> ! \forall integer k; 0 <= k < length ==> a[k] == b[k];
> 
> should be parsed as
> 
> ! (\forall integer k; (0 <= k < length ==> a[k] == b[k]));
> 

You're right. This was a bug in the parser of the logic. It is fixed in
the development version.
Thanks for the report.

Best regards,
-- 
Virgile Prevosto
Ing?nieur-Chercheur, CEA, LIST
Laboratoire de S?ret? des Logiciels
+33/0 1 69 08 82 98