implicit conversion of terms to predicates
ID0002148: This issue was created automatically from Mantis Issue 2148. Further discussion may take place here.
|ID0002148||Frama-C||Kernel > ACSL implementation||public||2015-07-17||2015-07-17|
|Product Version||Frama-C Sodium||Target Version||-||Fixed in Version||-|
ACSL 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?