--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on May 2015 ---
Hi, No, chained comparisons are not allowed as such in terms. From my understanding, the syntax of ACSL terms was chosen to be as similar as possible to the one of side-effects-free C expressions. In C, x < y < z is parsed as the (misleading) (x < y) < z, which is too different from the meaning we give to x < y < z in specifications. That being said, as you noticed, x < y < z is indeed accepted in a term position by Frama-C. In this case, the _predicate_ is cast from boolean to integer, and used as a term. This is documented in section 2.2.3 of the ACSL manual. HTH, On Sat, May 23, 2015 at 8:52 PM, cok at frontiernet.net <cok at frontiernet.net> wrote: > The ACSL1.9 document defines and discusses chained comparisons: > Fig 2.2 gives a rule for pred as term ( rel-op term )+ > > But Fig 2.1 does not give a corresponding rule for terms. > It just says that a term can be term bin-op term > > Is it intended that chained comparisons may be used only in predicate > position? > Or is it implicitly allowed for terms also since term bin-op term bin-op > term > parses as an appropriate tree? > > Thanks, > > - David > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -- Boris -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150528/f1bb093c/attachment.html>