suggest to insert implicit cast of logic function's expression to return type
ID0001577: This issue was created automatically from Mantis Issue 1577. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001577 | Frama-C | Kernel | public | 2013-11-28 | 2013-12-17 |
| Reporter | Jochen | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Fluorine-20130601 | Target Version | - | Fixed in Version | - |
Description :
The 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.