--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on November 2014 ---
Hi, The ACSL manual version 1.8 ( http://frama-c.com/download/acsl.pdf ) explains a little bit about typing. The document mentions that "There is an implicit promotion from integers to booleans" (in section 2.2.3 ) . But I found that, that is not always true. For example : Consider below predicate: /*@ predicate is_false{L}(*boolean* i) = i == \false ;*/ If a call is made to this predicate as below: /*@ ensures is_false(*1*) ; */ It throws error: invalid implicit conversion from Z to B in annotation. Also I noticed that not all implicit coercions are restricted in such cases. for example conversion from integers to reals is allowed. For example: Consider below logic function: /*@ logic integer get_sign(*real* x) = x >= 0.0 ? 1 : ( x<0.0 ? -1 : 0) ; */ Calling this function as below if fine: /*@ ensures get_sign(1); */ or int a =1; char b = 'b'; /*@ ensures get_sign(a); ensures get_sign(b); */ are fine. Also some other implicit coercions which are fine in ACSL expressions, are not fine in function definition. For example implicit coercion from int to double. For a C function like: void test(*double *d){ .... } A requires clause like : /*@ requires d > (*int*)1; */ is fine. But in a logic function: /*@ logic *double* get_sign(integer x) = (*int*)(x > 0.0 ? 1 : (x<0.0 ? -1 : 0)) ; */ ( Note: this is contrived example ) it gives error: invalid implicit conversion from 'int' to 'double' in annotation. But again some implicit coercions are allowed in function definition. Like conversion from char to int or short to int is allowed. /*@ logic*int* get_sign(integer x) = (*char* )(x > 0.0 ? 1 : (x<0.0 ? -1 : 0)) ; */ doesn't throw error. It looks like there is a lot of inconsistency in implicit type coercions. Is there any document which explains the implicit type coercions allowed in frama-c ? Thanks, Gunjan -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141113/726319e6/attachment.html>