2021-02-24 19:22 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000530Frama-CPlug-in > jessiepublic2010-12-18 11:19
Reporteragoodloe 
Assigned Tocmarche 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101202-beta2 
Summary0000530: crash
Description/usr/include/libkern/i386/_OSByteOrder.h:59:[jessie] failure: Unexpected failure.
                  Please submit bug report (Ref. "interp.ml:1920:13").
[kernel] The full backtrace is:
         Raised at file "src/kernel/log.ml", line 506, characters 30-31
         Called from file "src/kernel/log.ml", line 500, characters 2-9
         Re-raised at file "src/kernel/log.ml", line 503, characters 8-9
         Called from file "src/lib/type.ml", line 746, characters 40-45
         Called from file "queue.ml", line 134, characters 6-20
         Called from file "src/kernel/boot.ml", line 50, characters 4-20
         Called from file "src/kernel/cmdline.ml", line 170, characters 4-8
         
         Plug-in jessie aborted because of an internal error.
         Please report as 'crash' at http://bts.frama-c.com
Additional InformationI was trying to see if Frama-c/Jessie could help verify properties of code produced by a code generator we are building. Maybe the c code produced is too twisted for jessie.
TagsNo tags attached.
Attached Files
  • c file icon t3.c (4,463 bytes) 2010-07-07 00:24 -
    #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-07 00:24 +

-Relationships
related to 0000541closedvirgile When using -pp-annot and including stdbool.h, can't parse \false in annotations 
+Relationships

-Notes

~0000984

pascal (reporter)

Your C file doesn't seem too horrible at all, and the error comes from one of the system headers on your computer, so things may go differently on ours. System header contain all sorts of horrible things, and never the same ones from one system to the next (and do you really intend to verify the code for use on this particular computer anyway?)

If you want generic, noncommittal header files, we provide quite a few of the C99/POSIX standard ones in .../share/frama-c/libc/. Since you have attached your C file, I will make a try myself when I get the chance.

~0001002

pascal (reporter)

Of course, it would help greatly if we distributed replacement headers that Frama-C can actually parse.

I used the commandline:

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

In order to circumvent a bunch of errors of the form below, I had to patch one of the Frama-C substitution header file.


[kernel] preprocessing with "gcc -I/usr/local/Frama-C_B/share/frama-c/libc -C -E -dD t3.c"
/usr/local/Frama-C_B/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.


The patch follows below. Once this problem was out of the way, the next, and probably last (but one never knows, one never knows) issue appears to be that of recognition of the C99 bool type by Jessie:

Manzana:t3 pascal$ frama-c -jessie -cpp-command "gcc -I/usr/local/Frama-C_B/share/frama-c/libc -C -E " t3.c
[kernel] preprocessing with "gcc -I/usr/local/Frama-C_B/share/frama-c/libc -C -E -dD t3.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir t3.jessie
[jessie] File t3.jessie/t3.jc written.
[jessie] File t3.jessie/t3.cloc written.
[jessie] Calling Jessie tool in subdir t3.jessie
File "t3.jc", line 36, characters 2-7: typing error: unknown type _bool
[jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs t3.cloc t3.jc


I guess that Claude is the only person who can tell if (C99) bool support in Jessie in a long way off, but meanwhile, while not continue the experiment by putting an enum definition instead in stdbool.h (using the right macros so as not to clash with the C99 bool type)?

Good luck...
_________________________________


Manzana:t3 pascal$ diff -u ~/ppc/share/libc/stdlib.h /usr/local/Frama-C_B/share/frama-c/libc/stdlib.h
--- /Users/pascal/ppc/share/libc/stdlib.h 2010-04-26 18:42:31.000000000 +0200
+++ /usr/local/Frama-C_B/share/frama-c/libc/stdlib.h 2010-07-13 06:08:21.000000000 +0200
@@ -124,7 +124,7 @@
 
 /* ISO C: 7.20.4 */
 
-/*@ terminates \false; */
+/* @ terminates \false; */
 void abort(void);
 
 /*@ assigns \result \from \nothing ;*/
@@ -134,16 +134,16 @@
 int at_quick_exit(void (*func)(void));
 
 /*@
- terminates \false;
+// terminates \false;
   assigns \nothing;
- ensures \false;
+// ensures \false;
 */
 void exit(int status);
 
 /*@
- terminates \false;
+// terminates \false;
   assigns \nothing;
- ensures \false;
+// ensures \false;
 */
 void _Exit(int status);
 
@@ -153,9 +153,9 @@
 char *getenv(const char *name);
 
 /*@
- terminates \false;
+// terminates \false;
   assigns \nothing;
- ensures \false; */
+// ensures \false; */
 void quick_exit(int status);
 
 /*@ assigns \result \from string[..]; */
Manzana:t3 pascal$

~0001003

pascal (reporter)

Alwyn:

Actually, the parsing error that I first bumped into only happens when using the -jessie option. I will investigate a little further and report it here when I understand it better.

It all depends what kind of properties you intended to check, but with the commandline:

frama-c-gui -cpp-command "gcc -I/usr/local/Frama-C_B/share/frama-c/libc -C -E " t3.c -val -slevel 100

the value analysis is precise enough to tell that there are no run-time errors in the execution of the program, and to give variation ranges for some variables and structure fields.

~0001315

cmarche (developer)


Why 2.28 outputs a better error message. The problem is is the specification: equality over structures are not supported and should be replaced by the equality of all the fields (e.g. defined as logic predicate)
+Notes

-Issue History
Date Modified Username Field Change
2010-07-07 00:24 agoodloe New Issue
2010-07-07 00:24 agoodloe Status new => assigned
2010-07-07 00:24 agoodloe Assigned To => cmarche
2010-07-07 00:24 agoodloe File Added: t3.c
2010-07-08 16:04 pascal Note Added: 0000984
2010-07-13 06:22 pascal Note Added: 0001002
2010-07-13 06:45 pascal Note Added: 0001003
2010-07-30 16:34 virgile Relationship added related to 0000541
2010-12-16 16:48 cmarche Note Added: 0001315
2010-12-16 16:48 cmarche Status assigned => resolved
2010-12-16 16:48 cmarche Resolution open => fixed
2010-12-18 11:18 signoles Fixed in Version => Frama-C Carbon-20101202-beta2
2010-12-18 11:19 signoles Status resolved => closed
+Issue History