Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 208
    • Issues 208
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #575

Closed
Open
Created Dec 05, 2015 by David Cok@cokDeveloper

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?

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking