Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002195Frama-CKernel > ACSL implementationpublic2015-12-05 14:512015-12-06 05:16 
Assigned Tovirgile 
PlatformOSOS Version
Product VersionFrama-C Sodium 
Target VersionFixed in Version 
Summary0002195: ambiguity with consecutive comparison and ternary expressions
DescriptionThe 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?
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006111) (reporter)
2015-12-05 15:33

This should have been marked against Sodium (ACSL 1.9) not Neon. - dcok

- Issue History
Date Modified Username Field Change
2015-12-05 14:51 New Issue
2015-12-05 14:51 Status new => assigned
2015-12-05 14:51 Assigned To => virgile
2015-12-05 15:33 Note Added: 0006111
2015-12-06 05:16 signoles Product Version Frama-C Neon-20140301 => Frama-C Sodium

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker