2021-03-03 03:52 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000489Frama-CKernelpublic2014-02-12 16:55
Reporterpuccetti 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000489: Cint64 user constants have no textual representation
DescriptionInteger literal constants are represented in CIL by the following type:

type constant =
  | CInt64 of int64 * ikind * string option
...

But the user-defined integer constants have an empty textual representation (3rd component of type above).
Additional InformationAn example file is appended.
TagsNo tags attached.
Attached Files
  • c file icon m10_1.c (3,678 bytes) 2010-05-28 10:03 -
    #include "misra.h"
    
    void foo1(uint8_t x) {};
    
    int16_t t1(void)
    {
      uint8_t u8a, u8b, u8c;
      int8_t s8a, s8b;
      uint16_t u16a;
      int16_t s16a;
      int32_t s32a;
      float f32a;
      double f64a;
      uint8_t azertyuiopqsdfghjklmwxcvbnazerty=1; /* not compliant with 1.4 */
       foo1(u8a);            /* compliant     */
       foo1(u8a + u8b);      /* compliant     */
       foo1(s8a);            /* not compliant */
       foo1(u16a);           /* not compliant */
       foo1(2);              /* not compliant */
       foo1(2U);             /* compliant     */
       foo1((uint8_t)2);     /* compliant     */
       /*... s8a + u8a         /* not compliant */
       /*... s8a + (int8_t)u8a /* compliant     */
       s8b = u8a;            /* not compliant */
       /*... u8a + 5           /* not compliant */
       /*... u8a + 5U          /* compliant     */
       /*... u8a + (uint8_t)5  /* compliant     */
       u8a = u16a+azertyuiopqsdfghjklmwxcvbnazerty;           /* not compliant */
       u8a = (uint8_t)u16a;  /* compliant     */
       u8a = 5UL;            /* not compliant */
       /*... u8a + 10UL        /* compliant     */
       u8a = 5U;             /* compliant     */
       /*... u8a + 3           /* not compliant */
       /*... u8a >> 3          /* compliant     */
       /*... u8a >> 3U         /* compliant     */
    
       /*... s32a + 80000      /* compliant     */
       /*... s32a + 80000L     /* compliant     */
       f32a = f64a;          /* not compliant */
       f32a = 2.5;           /* not compliant -
                                unsuffixed floating
                                constants are of type
                                double        */
       u8a  = u8b +  u8c;    /* compliant     */
       s16a = u8b +  u8b;    /* not compliant */
       s32a = u8b +  u8c;    /* not compliant */
       f32a = 2.5F;          /* compliant     */
       u8a  = f32a;          /* not compliant */
       s32a = 1.0;           /* not compliant */
       s32a = u8b +  u8c;    /* not compliant */
       f32a = 2.5F;          /* compliant     */
       u8a  = f32a;          /* not compliant */
       s32a = 1.0;           /* not compliant */
       f32a = 1;             /* not compliant */
       f32a = s16a;          /* not compliant */
       /*... f32a + 1                  /* not compliant */
       /*... f64a * s32a               /* not compliant */
       /*...*/
       return (s32a);                /* not compliant */
       /*...*/
       return (s16a);                /* compliant     */
       /*...*/
       return (20000);               /* compliant     */
       /*...*/
       return (20000L);              /* not compliant */
       /*...*/
       return (s8a);                 /* not compliant */
       /*...*/
       return (u16a);                /* not compliant */
    };
    
    int16_t foo2(void)
    {
      uint8_t u8a, u8b;
      int8_t s8a;
      uint16_t u16a,u16b;
      int16_t s16a,s16b;
      int32_t s32a,s32b;
      uint32_t u32a;
      float f32a,f32b;
      double f64a,f64b ;
    
       /*... (u16a + u16b) + u32a      /* not compliant */
       /*... s32a + s8a + s8b          /* compliant     */
       /*... s8a + s8b + s32a          /* not compliant */
       f64a = f32a + f32b;           /* not compliant */
       f64a = f64b + f32a;           /* compliant     */
       f64a = s32a / s32b;           /* not compliant */
       u32a = u16a + u16a;           /* not compliant */
       s16a = s8a;                   /* compliant     */
       s16a = s16b + 20000;          /* compliant     */
       s32a = s16a + 20000;          /* not compliant */
       s32a = s16a + (int32_t)20000; /* compliant     */
       u16a = u16b + u8a;            /* compliant     */
       foo1(u16a);                   /* not compliant */
       foo1(u8a + u8b);              /* compliant     */
       /*...*/
       return s16a;                  /* compliant     */
       /*...*/
       return s8a;                   /* not compliant */
    }
    
    c file icon m10_1.c (3,678 bytes) 2010-05-28 10:03 +

-Relationships
+Relationships

-Notes
There are no notes attached to this issue.
+Notes

-Issue History
Date Modified Username Field Change
2010-05-28 10:03 puccetti New Issue
2010-05-28 10:03 puccetti File Added: m10_1.c
2010-05-28 10:08 virgile Status new => assigned
2010-05-28 10:08 virgile Assigned To => virgile
2010-05-28 10:09 virgile Status assigned => acknowledged
2010-05-28 19:11 svn
2010-05-31 09:22 svn
2010-05-31 09:25 virgile Status acknowledged => resolved
2010-05-31 09:25 virgile Resolution open => fixed
2010-12-10 15:45 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:36 signoles Status resolved => closed
2013-12-19 01:13 Source_changeset_attached => framac master dd0da2a1
2013-12-19 01:13 Source_changeset_attached => framac master cefe1e28
2014-02-12 16:55 Source_changeset_attached => framac stable/neon dd0da2a1
2014-02-12 16:55 Source_changeset_attached => framac stable/neon cefe1e28
+Issue History