Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001577Frama-CKernelpublic2013-11-28 13:542013-12-17 17:15
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeverityfeatureReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in Version 
Summary0001577: suggest to insert implicit cast of logic function's expression to return type
DescriptionThe body expression "(i + 1)" of the Acsl logic function "mySuccA" could by tacitly casted to "mySuccA"'s return type, viz. "char". This would be similar to the treatment in C code (function "mySuccC"). Currently, Frama-C reports a user typing error for the former, but not for the latter. Probably, this is not proper bug but compatible with the Acsl description. I just wanted to suggest to think about adapting the Ascl semantics here to the C semantics, which is more convenient for the user.
TagsNo tags attached.
Attached Filesc file icon char.c [^] (114 bytes) 2013-11-28 13:54 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2013-11-28 13:54 Jochen New Issue
2013-11-28 13:54 Jochen File Added: char.c
2013-12-17 17:15 signoles Status new => assigned
2013-12-17 17:15 signoles Assigned To => virgile


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker