Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Implicit Type Coercions

  • Subject: [Frama-c-discuss] Implicit Type Coercions
  • From: gaggarwal at grammatech.com (Gunjan Aggarwal)
  • Date: Thu, 13 Nov 2014 14:38:46 -0500
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>