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
Reporterdcok@grammatech.com 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityN/A
StatusassignedResolutionopen 
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)
dcok@grammatech.com (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 dcok@grammatech.com New Issue
2015-12-05 14:51 dcok@grammatech.com Status new => assigned
2015-12-05 14:51 dcok@grammatech.com Assigned To => virgile
2015-12-05 15:33 dcok@grammatech.com Note Added: 0006111
2015-12-06 05:16 signoles Product Version Frama-C Neon-20140301 => Frama-C Sodium


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker