Frama-C Bug Tracking System - Frama-C
View Issue Details
0002148Frama-CKernel > ACSL implementationpublic2015-07-17 18:122015-07-17 18:12
dcok@grammatech.com 
virgile 
normalmajoralways
assignedopen 
Frama-C Sodium 
 
0002148: implicit conversion of terms to predicates
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?
No tags attached.
Issue History
2015-07-17 18:12dcok@grammatech.comNew Issue
2015-07-17 18:12dcok@grammatech.comStatusnew => assigned
2015-07-17 18:12dcok@grammatech.comAssigned To => virgile

There are no notes attached to this issue.