[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/misc/widen_hints2.c (with preprocessing)
/* Generated by Frama-C */
typedef unsigned int size_t;
typedef int wchar_t;
struct __fc_div_t {
   int quot ;
   int rem ;
};
typedef struct __fc_div_t div_t;
struct __fc_ldiv_t {
   long quot ;
   long rem ;
};
typedef struct __fc_ldiv_t ldiv_t;
struct __fc_lldiv_t {
   long long quot ;
   long long rem ;
};
typedef struct __fc_lldiv_t lldiv_t;
/*@ assigns \result;
    assigns \result \from *(nptr + (..)); */
extern double atof(char const *nptr);

/*@ assigns \result;
    assigns \result \from *(nptr + (..)); */
extern int atoi(char const *nptr);

/*@ assigns \result;
    assigns \result \from *(nptr + (..)); */
extern long atol(char const *nptr);

/*@ assigns \result;
    assigns \result \from *(nptr + (..)); */
extern long long atoll(char const *nptr);

/*@ assigns \result, *endptr;
    assigns \result \from *(nptr + (0 ..));
    assigns *endptr \from nptr, *(nptr + (0 ..));
 */
extern double strtod(char const *nptr, char **endptr);

/*@ assigns \result, *endptr;
    assigns \result \from *(nptr + (0 ..));
    assigns *endptr \from nptr, *(nptr + (0 ..));
 */
extern float strtof(char const *nptr, char **endptr);

/*@ assigns \result, *endptr;
    assigns \result \from *(nptr + (0 ..));
    assigns *endptr \from nptr, *(nptr + (0 ..));
 */
extern long double strtold(char const *nptr, char **endptr);

/*@ assigns \result, *endptr;
    assigns \result
      \from (indirect: nptr), (indirect: *(nptr + (0 ..))), (indirect: base);
    assigns *endptr
      \from nptr, (indirect: *(nptr + (0 ..))), (indirect: endptr),
            (indirect: base);
    
    behavior null_endptr:
      assumes endptr ≡ \null;
      assigns \result;
      assigns \result
        \from (indirect: nptr), (indirect: *(nptr + (0 ..))),
              (indirect: base);
    
    behavior nonnull_endptr:
      assumes endptr ≢ \null;
      requires \valid(endptr);
      ensures \initialized(\old(endptr));
      ensures \subset(*\old(endptr), \old(nptr) + (0 ..));
      assigns \result, *endptr;
      assigns \result
        \from (indirect: nptr), (indirect: *(nptr + (0 ..))),
              (indirect: base);
      assigns *endptr
        \from nptr, (indirect: *(nptr + (0 ..))), (indirect: endptr),
              (indirect: base);
    
    complete behaviors nonnull_endptr, null_endptr;
    disjoint behaviors nonnull_endptr, null_endptr;
 */
extern long strtol(char const *nptr, char **endptr, int base);

/*@ assigns \result, *endptr;
    assigns \result \from *(nptr + (0 ..)), base;
    assigns *endptr \from nptr, *(nptr + (0 ..)), base;
 */
extern long long strtoll(char const *nptr, char **endptr, int base);

/*@ assigns \result, *endptr;
    assigns \result \from *(nptr + (0 ..)), base;
    assigns *endptr \from nptr, *(nptr + (0 ..)), base;
 */
extern unsigned long strtoul(char const *nptr, char **endptr, int base);

/*@ assigns \result, *endptr;
    assigns \result \from *(nptr + (0 ..)), base;
    assigns *endptr \from nptr, *(nptr + (0 ..)), base;
 */
extern unsigned long long strtoull(char const *nptr, char **endptr, int base);

/*@ ghost
  int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__)); */
unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ensures 0 ≤ \result ≤ __fc_rand_max;
    assigns \result, __fc_random_counter;
    assigns \result \from __fc_random_counter;
    assigns __fc_random_counter \from __fc_random_counter;
 */
extern int rand(void);

/*@ assigns __fc_random_counter;
    assigns __fc_random_counter \from seed; */
extern void srand(unsigned int seed);

/*@ requires nmemb * size ≤ 4294967295U; */
extern void *calloc(size_t nmemb, size_t size);

/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */

/*@
axiomatic dynamic_allocation {
  predicate is_allocable{L}(size_t n) 
    reads __fc_heap_status;
  
  }
 */
/*@ assigns __fc_heap_status, \result;
    assigns __fc_heap_status \from size, __fc_heap_status;
    assigns \result \from (indirect: size), (indirect: __fc_heap_status);
    allocates \result;
    
    behavior allocation:
      assumes is_allocable(size);
      ensures \fresh{Old, Here}(\result,\old(size));
      assigns __fc_heap_status, \result;
      assigns __fc_heap_status \from size, __fc_heap_status;
      assigns \result \from (indirect: size), (indirect: __fc_heap_status);
    
    behavior no_allocation:
      assumes ¬is_allocable(size);
      ensures \result ≡ \null;
      assigns \result;
      assigns \result \from \nothing;
      allocates \nothing;
    
    complete behaviors no_allocation, allocation;
    disjoint behaviors no_allocation, allocation;
 */
extern void *malloc(size_t size);

/*@ assigns __fc_heap_status;
    assigns __fc_heap_status \from __fc_heap_status;
    frees p;
    
    behavior deallocation:
      assumes p ≢ \null;
      requires freeable: \freeable(p);
      ensures \allocable(\old(p));
      assigns __fc_heap_status;
      assigns __fc_heap_status \from __fc_heap_status;
    
    behavior no_deallocation:
      assumes p ≡ \null;
      assigns \nothing;
      allocates \nothing;
    
    complete behaviors no_deallocation, deallocation;
    disjoint behaviors no_deallocation, deallocation;
 */
extern void free(void *p);

/*@ requires ptr ≡ \null ∨ \freeable(ptr);
    assigns __fc_heap_status, \result;
    assigns __fc_heap_status \from __fc_heap_status;
    assigns \result \from size, ptr, __fc_heap_status;
    frees ptr;
    allocates \result;
    
    behavior alloc:
      assumes is_allocable(size);
      ensures \fresh{Old, Here}(\result,\old(size));
      assigns \result;
      assigns \result \from size, __fc_heap_status;
      allocates \result;
    
    behavior dealloc:
      assumes ptr ≢ \null;
      assumes is_allocable(size);
      requires \freeable(ptr);
      ensures \allocable(\old(ptr));
      ensures \result ≡ \null ∨ \freeable(\result);
      frees ptr;
    
    behavior fail:
      assumes ¬is_allocable(size);
      ensures \result ≡ \null;
      assigns \result;
      assigns \result \from size, __fc_heap_status;
      allocates \nothing;
    
    complete behaviors fail, dealloc, alloc;
    disjoint behaviors alloc, fail;
    disjoint behaviors dealloc, fail;
 */
extern void *realloc(void *ptr, size_t size);

/*@ ensures \false;
    assigns \nothing; */
extern void abort(void);

/*@ assigns \result;
    assigns \result \from \nothing; */
extern int atexit(void (*func)(void));

/*@ assigns \result;
    assigns \result \from \nothing; */
extern int at_quick_exit(void (*func)(void));

/*@ ensures \false;
    assigns \nothing; */
extern  __attribute__((__noreturn__)) void exit(int status);

/*@ ensures \false;
    assigns \nothing; */
extern  __attribute__((__noreturn__)) void _Exit(int status);

/*@ ensures \result ≡ \null ∨ \valid(\result);
    assigns \result;
    assigns \result \from name;
 */
extern char *getenv(char const *name);

/*@ ensures \false;
    assigns \nothing; */
extern  __attribute__((__noreturn__)) void quick_exit(int status);

/*@ assigns \result;
    assigns \result \from *(string + (..)); */
extern int system(char const *string);

/*@ assigns *((char *)\result + (..));
    assigns *((char *)\result + (..))
      \from *((char *)key + (..)), *((char *)base + (..)), nmemb, size,
            *compar;
 */
extern void *bsearch(void const *key, void const *base, size_t nmemb,
                     size_t size, int (*compar)(void const *, void const *));

/*@ assigns *((char *)base + (..));
    assigns *((char *)base + (..))
      \from *((char *)base + (..)), nmemb, size, *compar;
 */
extern void qsort(void *base, size_t nmemb, size_t size,
                  int (*compar)(void const *, void const *));

/*@ requires abs_representable: (int)(-j) ≡ -j;
    assigns \result;
    assigns \result \from j;
 */
extern int abs(int j);

/*@ requires abs_representable: (long)(-j) ≡ -j;
    assigns \result;
    assigns \result \from j;
 */
extern long labs(long j);

/*@ requires abs_representable: (long long)(-j) ≡ -j;
    assigns \result;
    assigns \result \from j;
 */
extern long long llabs(long long j);

/*@ assigns \result;
    assigns \result \from numer, denom; */
extern div_t div(int numer, int denom);

/*@ assigns \result;
    assigns \result \from numer, denom; */
extern ldiv_t ldiv(long numer, long denom);

/*@ assigns \result;
    assigns \result \from numer, denom; */
extern lldiv_t lldiv(long long numer, long long denom);

/*@ assigns \result;
    assigns \result \from *(s + (0 ..)), n; */
extern int mblen(char const *s, size_t n);

/*@ assigns \result, *(pwc + (0 .. n - 1));
    assigns \result \from *(s + (0 .. n - 1)), n;
    assigns *(pwc + (0 .. n - 1)) \from *(s + (0 .. n - 1)), n;
 */
extern int mbtowc(wchar_t *pwc, char const *s, size_t n);

/*@ assigns \result, *(s + (0 ..));
    assigns \result \from wc;
    assigns *(s + (0 ..)) \from wc;
 */
extern int wctomb(char *s, wchar_t wc);

/*@ assigns \result, *(pwcs + (0 .. n - 1));
    assigns \result \from *(s + (0 .. n - 1)), n;
    assigns *(pwcs + (0 .. n - 1)) \from *(s + (0 .. n - 1)), n;
 */
extern size_t mbstowcs(wchar_t *pwcs, char const *s, size_t n);

/*@ assigns \result, *(s + (0 .. n - 1));
    assigns \result \from *(pwcs + (0 .. n - 1)), n;
    assigns *(s + (0 .. n - 1)) \from *(pwcs + (0 .. n - 1)), n;
 */
extern size_t wcstombs(char *s, wchar_t const *pwcs, size_t n);

int t[100];
int const x = 9;
int glob;
void f(void)
{
  int tf[100];
  int m;
  int n;
  m = 10;
  n = 33 + m;
  /*@ widen_hints "all", 88; */
  {
    int a;
    a = 0;
    while (a < n * 2 + 1) {
      {
        int b;
        b = 0;
        while (b < a) {
          tf[b] = 1;
          b ++;
        }
      }
      a ++;
    }
  }
  return;
}

void g(void)
{
  int tg[100];
  int m;
  int n;
  m = 10;
  n = 33 + m;
  {
    int ll;
    ll = 0;
    while (ll < n * 2 + 1) {
      {
        int kk;
        kk = 0;
        while (kk < ll) {
          tg[kk] = 1;
          kk ++;
        }
      }
      ll ++;
    }
  }
  return;
}

int y;
int main(void)
{
  int __retres;
  int y_0;
  int m;
  int n;
  m = 10;
  /*@ widen_hints global:m, 2;
        widen_hints y_0, 5; */
  n = 33 + m;
    {
      int a;
      a = 0;
      /*@ loop widen_hints a, 2; */
      while (a < n * 2 + 1) {
        /*@ widen_hints a, 88; */
        {
          int b;
          b = 0;
          while (b < a) {
            t[b] = 1;
            b ++;
          }
        }
        a ++;
      }
    }
    {
      int c;
      c = 0;
      /*@ loop widen_hints c, 88;
          loop widen_hints y_0, 1;
          loop widen_hints global:y_0, 2;
        */
        while (c < n * 2 + 1) {
          {
            int d;
            d = 0;
            while (d < c) {
              t[d] = 1;
              d ++;
            }
          }
          c ++;
        }
      }
      {
        int c_0;
        c_0 = 0;
        /*@ loop widen_hints c_0, 88; */
        while (c_0 < n * 2 + 1) {
          {
            int d_0;
            d_0 = 0;
            while (d_0 < c_0) {
              t[d_0] = 1;
              d_0 ++;
            }
          }
          c_0 ++;
        }
      }
      /*@ widen_hints glob, 88; */
      {
        glob = 0;
        while (glob < n * 2 + 1) {
          {
            int j;
            j = 0;
            while (j < glob) {
              t[j] = 1;
              j ++;
            }
          }
          glob ++;
        }
      }
      f();
      g();
      __retres = 0;
      return __retres;
    }