--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on January 2011 ---
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])); Instead, it produces a syntax error. Is the former expression parsed as (! \forall) ... ? That would be wrong. -- Regards, Boris