implicit conversion of terms to predicates
ID0002148: This issue was created automatically from Mantis Issue 2148. Further discussion may take place here.
|Kernel > ACSL implementation
|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?