2020-12-04 23:49 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000541Frama-CKernel > ACSL implementationpublic2014-02-12 16:55
Reporterpascal 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000541: When using -pp-annot and including stdbool.h, can't parse \false in annotations
DescriptionOn the attached program (that came from bug report 530), when the -pp-annot option is used, the \false in annotations cause problems.

Commandline (for me, adjust path as needed):

frama-c -pp-annot -cpp-command "gcc -I/usr/local/Frama-C_B/share/frama-c/libc -C -E " t3.c

Results:

[kernel] preprocessing with "gcc -I/usr/local/share/frama-c/libc -C -E -dD t3.c"
/usr/local/share/frama-c/libc/stdlib.h:127:[kernel] user error: lexical error, illegal character \
[kernel] user error: skipping file "t3.c" that has errors.
[kernel] Frama-C aborted because of an invalid user input.

More details are available at bug 530.
TagsNo tags attached.
Attached Files
  • c file icon t3.c (4,463 bytes) 2010-07-13 15:47 -
    #include <stdbool.h>
    #include <stdint.h>
    
    /* #include <stdio.h> */
    #include <stdlib.h>
    #include <string.h>
    
    unsigned long long rnd;
    uint32_t ext;
    
    
    static uint64_t __global_clock = 0;
    
    
    
    struct {  /* state */
      struct {  /* t3 */
        bool prophVal__b[3];
        int32_t prophVal__a[3];
        bool outputVal__b;
        int32_t outputVal__a;
        int32_t tmpSampleVal__ext_1;
        int32_t tmpSampleVal__ext_8;
      } t3;
    } state =
    {  /* state */
      {  /* t3 */
        /* prophVal__b */
        { true
        , false
        , false
        },
        /* prophVal__a */
        { 0L
        , 1L
        , 0L
        },
        /* outputVal__b */  false,
        /* outputVal__a */  0L,
        /* tmpSampleVal__ext_1 */  0L,
        /* tmpSampleVal__ext_8 */  0L
      }
    };
    
    /* t3.update__b */
    static void __r0() {
      bool __0 = true;
      int32_t __1 = 2L;
      uint64_t __2 = 0ULL;
      int32_t __3 = state.t3.prophVal__a[__2];
      int32_t __4 = __1 + __3;
      int32_t __5 = 5L;
      int32_t __6 = state.t3.tmpSampleVal__ext_1;
      int32_t __7 = __5 + __6;
      bool __8 = __4 < __7;
      uint64_t __9 = 2ULL;
      if (__0) {
      }
      state.t3.prophVal__b[__9] = __8;
    }
    
    /* t3.update__a */
    static void __r3() {
      bool __0 = true;
      uint64_t __1 = 0ULL;
      int32_t __2 = state.t3.prophVal__a[__1];
      int32_t __3 = state.t3.tmpSampleVal__ext_8;
      int32_t __4 = state.t3.tmpSampleVal__ext_1;
      int32_t __5 = __3 + __4;
      int32_t __6 = __3 + __5;
      int32_t __7 = __2 + __6;
      uint64_t __8 = 2ULL;
      if (__0) {
      }
      state.t3.prophVal__a[__8] = __7;
    }
    
    /* t3.output__b */
    static void __r1() {
      bool __0 = true;
      uint64_t __1 = 0ULL;
      bool __2 = state.t3.prophVal__b[__1];
      if (__0) {
      }
      state.t3.outputVal__b = __2;
    }
    
    /* t3.output__a */
    static void __r4() {
      bool __0 = true;
      uint64_t __1 = 0ULL;
      int32_t __2 = state.t3.prophVal__a[__1];
      if (__0) {
      }
      state.t3.outputVal__a = __2;
    }
    
    /* t3.sample__ext_1 */
    static void __r6() {
      bool __0 = true;
      int32_t __1 = ext;
      if (__0) {
      }
      state.t3.tmpSampleVal__ext_1 = __1;
    }
    
    /* t3.shiftArr__a */
    static void __r5() {
      bool __0 = true;
      uint64_t __1 = 2ULL;
      int32_t __2 = state.t3.prophVal__a[__1];
      uint64_t __3 = 1ULL;
      int32_t __4 = state.t3.prophVal__a[__3];
      uint64_t __5 = 0ULL;
      if (__0) {
      }
      state.t3.prophVal__a[__3] = __2;
      state.t3.prophVal__a[__5] = __4;
    }
    
    /* t3.shiftArr__b */
    static void __r2() {
      bool __0 = true;
      uint64_t __1 = 2ULL;
      bool __2 = state.t3.prophVal__b[__1];
      uint64_t __3 = 1ULL;
      bool __4 = state.t3.prophVal__b[__3];
      uint64_t __5 = 0ULL;
      if (__0) {
      }
      state.t3.prophVal__b[__3] = __2;
      state.t3.prophVal__b[__5] = __4;
    }
    
    /* t3.sample__ext_8 */
    static void __r7() {
      bool __0 = true;
      int32_t __1 = ext;
      if (__0) {
      }
      state.t3.tmpSampleVal__ext_8 = __1;
    }
    
    
    
    void t3() {
      {
        static uint8_t __scheduling_clock = 0;
        if (__scheduling_clock == 0) {
          __r0();  /* t3.update__b */
          __r3();  /* t3.update__a */
          __scheduling_clock = 8;
        }
        else {
          __scheduling_clock = __scheduling_clock - 1;
        }
      }
      {
        static uint8_t __scheduling_clock = 1;
        if (__scheduling_clock == 0) {
          __r1();  /* t3.output__b */
          __r4();  /* t3.output__a */
          __r6();  /* t3.sample__ext_1 */
          __scheduling_clock = 8;
        }
        else {
          __scheduling_clock = __scheduling_clock - 1;
        }
      }
      {
        static uint8_t __scheduling_clock = 2;
        if (__scheduling_clock == 0) {
          __r5();  /* t3.shiftArr__a */
          __scheduling_clock = 8;
        }
        else {
          __scheduling_clock = __scheduling_clock - 1;
        }
      }
      {
        static uint8_t __scheduling_clock = 3;
        if (__scheduling_clock == 0) {
          __r2();  /* t3.shiftArr__b */
          __scheduling_clock = 8;
        }
        else {
          __scheduling_clock = __scheduling_clock - 1;
        }
      }
      {
        static uint8_t __scheduling_clock = 8;
        if (__scheduling_clock == 0) {
          __r7();  /* t3.sample__ext_8 */
          __scheduling_clock = 8;
        }
        else {
          __scheduling_clock = __scheduling_clock - 1;
        }
      }
    
      __global_clock = __global_clock + 1;
    
    }
    
    int main(int argc, char *argv[]) {
      if (argc != 2) {
        return 1;
      }
      /* rnd = atoi(argv[1]);*/
      rnd = 10;
    
      state.t3.tmpSampleVal__ext_8 = ext;
      state.t3.tmpSampleVal__ext_1 = ext;
      int i = 0;
      for(; i < rnd ; i++) {
        int j = 0;
        for (; j < 9 ; j++) {
          t3();
        }
    /*    printf("period: %i   ", i);
        printf("a: %ld   ", state.t3.outputVal__a);
        printf("b: %hu   ", state.t3.outputVal__b);
        printf("\n" );
        fflush(stdout); */
      }
      return EXIT_SUCCESS;
    }
    
    
    c file icon t3.c (4,463 bytes) 2010-07-13 15:47 +

-Relationships
related to 0000530closedcmarche crash 
+Relationships

-Notes

~0001008

monate (reporter)

The problem comes from the tokenization rules of the preprocessor:

\ident is tokenized as \ ident and therefore macro expansion may occur on ident.

In the above case we have :
===
#define false 0
//@ terminates \false ;
===

It is preprocessed as: terminates \0
This will also break for all \ prefixed identifiers in logic.

~0001023

virgile (developer)

Logic pre-pre-processor might do something about it.

~0001024

virgile (developer)

BTW, I'm making a test case from comment 1008. t3.c does not contain any annotation, much less a \false somewhere.

~0001025

pascal (reporter)

I strongly disagree on the t3.c comment.

I think it would be very useful to have a test based on t3.c, containing

#include <stdbool.h>
#include <stdint.h>
#include <stdlib.h>
#include <string.h>

because this happens quite a bit more often than whatever specialized test case you are writing.

We could even #include <limit.h> and use any of the macros defined there. That would again be representative of what typical programs do.

~0001026

virgile (developer)

There seems to be a misunderstanding. I'm perfectly happy with including stdbool. My remark was that t3.c alone is useless for detecting the bug as long as it does not contain any annotation. The #include in themselves cause no harm.

~0001027

pascal (reporter)

Yes they do, try the commandline:

frama-c -pp-annot -cpp-command "gcc -I/usr/local/Frama-C_B/share/frama-c/libc -C -E " t3.c

Adjust path as needed.

~0001028

virgile (developer)

OK, I see it now, I didn't think about annotations in included files, sorry. Nevertheless, the main interest of t3.c are the #include, the code itself is just a distraction (from bug 541 point of view).
+Notes

-Issue History
Date Modified Username Field Change
2010-07-13 15:47 pascal New Issue
2010-07-13 15:47 pascal Status new => assigned
2010-07-13 15:47 pascal Assigned To => virgile
2010-07-13 15:47 pascal File Added: t3.c
2010-07-16 13:26 pascal Summary When using -jessie, can't parse \ in annotations => When using -pp-annot, can't parse \ in annotations
2010-07-16 13:26 pascal Description Updated
2010-07-16 13:46 pascal Summary When using -pp-annot, can't parse \ in annotations => When using -pp-annot and including stdbool.h, can't parse \false in annotations
2010-07-16 15:10 monate Note Added: 0001008
2010-07-30 16:34 virgile Note Added: 0001023
2010-07-30 16:34 virgile Status assigned => acknowledged
2010-07-30 16:34 virgile Relationship added related to 0000530
2010-07-30 16:45 virgile Note Added: 0001024
2010-07-30 16:56 pascal Note Added: 0001025
2010-07-30 17:17 virgile Note Added: 0001026
2010-07-30 17:21 pascal Note Added: 0001027
2010-07-30 17:31 virgile Note Added: 0001028
2010-08-16 14:39 svn
2010-08-16 14:39 svn Status acknowledged => resolved
2010-08-16 14:39 svn 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:12 Source_changeset_attached => framac master 5238d796
2014-02-12 16:55 Source_changeset_attached => framac stable/neon 5238d796
+Issue History