--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on January 2011 ---
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