2021-01-21 06:35 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001577Frama-CKernelpublic2013-12-17 17:15
Assigned Tovirgile 
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 Files
  • c file icon char.c (114 bytes) 2013-11-28 13:54 -
    //@ logic char mySuccA(char i) =              (i + 1);
              char mySuccC(char i) { return       (i + 1); }
    c file icon char.c (114 bytes) 2013-11-28 13:54 +


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
+Issue History