Frama-C Bug Tracking System - Frama-C
View Issue Details
0002195Frama-CKernel > ACSL implementationpublic2015-12-05 14:512015-12-06 05:16 
Frama-C Sodium 
0002195: ambiguity with consecutive comparison and ternary expressions
The ACSL grammar allows two forms of ternary expressions for predicates: term ? pred : pred pred ? pred : pred But the interpretation of consecutive comparisons depends on whether the expression is in term or predicate position. Thus the predicate (i == j < k) ? (\true==>\\true) ? (\true==>\false) is fundamentally ambiguous in the grammar. If the condition is a predicate, it is equivalent to ((i == j) && (j < k)) ? ... As a term it is equivalent to ((i == j) < k) ? Depending on the types of i, j, and k, it may not typecheck correctly as either a term or predicate - but does, for example, if all three are ints. However, it would be really bad design if the grammar parser depended on the types of expressions. Is this construct deemed illegal, or is it resolved in favor of one form or the other?
No tags attached.
Issue History
2015-12-05 14:51dcok@grammatech.comNew Issue
2015-12-05 14:51dcok@grammatech.comStatusnew => assigned
2015-12-05 14:51dcok@grammatech.comAssigned To => virgile
2015-12-05 15:33dcok@grammatech.comNote Added: 0006111
2015-12-06 05:16signolesProduct VersionFrama-C Neon-20140301 => Frama-C Sodium

2015-12-05 15:33   
This should have been marked against Sodium (ACSL 1.9) not Neon. - dcok