ambiguity with consecutive comparison and ternary expressions
ID0002195: This issue was created automatically from Mantis Issue 2195. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002195 | Frama-C | Kernel > ACSL implementation | public | 2015-12-05 | 2015-12-06 |
| Reporter | dcok@grammatech.com | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | major | Reproducibility | N/A |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Sodium | Target Version | - | Fixed in Version | - |
Description :
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?