Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002148Frama-CKernel > ACSL implementationpublic2015-07-17 18:122015-07-17 18:12
Reporterdcok@grammatech.com 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Sodium 
Target VersionFixed in Version 
Summary0002148: implicit conversion of terms to predicates
DescriptionACSL distinguishes carefully between terms and predicates. For example, a predicate (e.g. \valid(...) ) cannot be placed in a term position, such as the argument of a cast. However, clauses such as 'requires 1;' are accepted by Frama-C, even though the 1.9 grammar nowhere permits terms to be implicitly converted to predicates. Integer-typed terms maybe implicitly converted to boolean terms, but there is no indication that terms are converted to predicates. Is this an oversight in the grammar? or does Frama-C accept more than the grammar as a convenience?
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2015-07-17 18:12 dcok@grammatech.com New Issue
2015-07-17 18:12 dcok@grammatech.com Status new => assigned
2015-07-17 18:12 dcok@grammatech.com Assigned To => virgile


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker