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.
|Product Version||Frama-C Fluorine-20130601||Target Version||-||Fixed in Version||-|
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.