Skip to content
Snippets Groups Projects
Forked from pub / open-source-case-studies
204 commits behind the upstream repository.
framac.ast 8.15 KiB
/* Generated by Frama-C */
#include "errno.h"
#include "stdarg.h"
#include "stddef.h"
#include "stdint.h"
#include "stdio.h"
#include "stdlib.h"
#include "string.h"
#include "strings.h"
typedef uint8_t u1;
typedef uint16_t u2;
typedef uint32_t u4;
u4 k;
u4 l;
u4 n;
u1 m;
u1 o;
u1 p;
u1 q;
u1 r;
u1 s;
u1 *t;
u1 *u;
u2 A(u1 *c)
{
  u2 __retres;
  __retres = (unsigned short)((int)*(c + ! (! c)) | ((int)((unsigned short)*c) << l));
  return __retres;
}

void B(u1 *c, u2 a)
{
  u1 *tmp;
  tmp = c;
  c ++;
  *tmp = (unsigned char)((int)a >> l);
  *c = (unsigned char)a;
  return;
}

int C(u1 *c, u4 *a)
{
  int __retres;
  u1 b;
  u4 tmp;
  u4 tmp_0;
  u1 d = (unsigned char)k;
  tmp = l;
  l -= (u4)1;
  s = (unsigned char)tmp;
  tmp_0 = k;
  k += (u4)1;
  *a = tmp_0;
  while ((int)d < (int)s >> k) {
    b = *(c + d);
    *a |= (unsigned int)((int)b & (int)p);
    if (! ((int)b >> l)) {
      u4 tmp_1;
      tmp_1 = k;
      k -= (u4)1;
      d = (unsigned char)((u4)d + tmp_1);
      l = (unsigned int)s;
      __retres = (int)d;
      goto return_label;
    }
    *a <<= l;
    d = (unsigned char)((int)d + 1);
  }
  exit(! k);
  __retres = (int)p;
  return_label: return __retres;
}

u1 D(u4 a)
{
  u1 __retres;
  u4 tmp;
  tmp = k;
  k += (u4)1;
  u1 b = (unsigned char)tmp;
  u1 c = (unsigned char)(l - k);
  if (a) {
    b = (unsigned char)k;
    while (1) {
      a >>= k;
      if (! a) break;
      b = (unsigned char)((int)b + 1);
    }
  }
  if (k) k = (unsigned int)(! k); else k = k;
  __retres = (unsigned char)((int)b / (int)c + ! (! ((int)b % (int)c)));
  return __retres;
}

int F(u4 a, u1 *c)
{
  int __retres;
  u4 tmp_0;
  u1 b = D(a);
  tmp_0 = l;
  l -= (u4)1;
  *c = (unsigned char)((u4)s - tmp_0);
  r = (unsigned char)((u4)q / n);
  if (! a) {
    __retres = (int)b;
    goto return_label;
  }
  if ((int)b > (int)r) exit((int)o);
  c += (int)b;
  c --;
  while (a) {
    *c = (unsigned char)(a & (unsigned int)p);
    a >>= l;
    c --;
  }
  l = (unsigned int)s;
  __retres = (int)b;
  return_label: return __retres;
}

u1 *G(u1 *c, u1 *a)
{
  u1 *__retres;
  u4 d;
  u1 b;
  u1 e;
  if ((int)m < (int)p) m = (unsigned char)((int)p << (int)q); else m = m;
  if ((u4)q < n + (u4)o) q = (unsigned char)((int)p >> (int)q); else 
                                                                  q = q;
  e = *c;
  if ((int)e == (int)m) goto _LOR;
  else 
    if ((int)e == (int)m + (int)q) {
      _LOR:
      {
        int tmp;
        *a = (unsigned char)k;
        c ++;
        tmp = C(c,& d);
        c += tmp;
        __retres = c + d;
        goto return_label;
      }
    }
  if ((int)e == ((int)m | (int)p)) {
    int tmp_0;
    *a = (unsigned char)k;
    c ++;
    c ++;
    tmp_0 = C(c,& d);
    c += tmp_0;
    __retres = c + d;
    goto return_label;
  }
  l /= (u4)o;
  if ((int)e >> (int)q) {
    b = *c;
    c ++;
    *a = b;
  }
  else b = *a;
  e = (unsigned char)((int)b >> l);
  if ((int)e < (int)s) exit((int)n);
  else 
    if ((u4)e > l + (u4)s) exit((int)n);
  if ((u4)e != l + (u4)s) 
    if ((u4)e != l + (u4)o) c ++;
  c ++;
  l = (unsigned int)s;
  __retres = c;
  return_label: return __retres;
}

u1 *H(u1 *c, u4 *a)
{
  u4 b;
  u4 e;
  u1 *d;
  u2 tmp;
  u2 tmp_0;
  u4 h = (unsigned int)q;
  u4 i = (unsigned int)m;
  u1 f = (unsigned char)k;
  *a = k;
  q = (unsigned char)((u4)q / n);
  m = (unsigned char)(((int)p - (int)m) + (int)p / (int)m);
  if ((int)*(c + n) != (int)m) exit((int)q);
  tmp = A(c + (int)q);
  tmp_0 = A(c + ((int)m >> (int)q));
  b = ((unsigned int)tmp << (int)q * (int)q) | (unsigned int)tmp_0;
  c += l;
  d = c + b;
  while (c < d) {
    int tmp_1;
    tmp_1 = C(c,& e);
    c += tmp_1;
    *a += e;
    c = G(c,& f);
  }
  q = (unsigned char)h;
  m = (unsigned char)i;
  return c;
}

u4 I(u1 *c, u4 a)
{
  u4 e;
  u4 b;
  u4 d = k;
  e = k;
  while (e < a) {
    c = H(c,& b);
    if (b > d) d = b;
    e += (u4)1;
  }
  return d;
}

u1 *J(u1 *c, u4 a, u4 b)
{
  u1 *__retres;
  u1 d;
  u1 e;
  if (l > (u4)o) {
    s = (unsigned char)((int)s - 1);
    o = (unsigned char)(((int)s - (int)o) << (int)r);
    l = (unsigned int)((int)p % ((int)s + (int)o));
    r = (unsigned char)((u4)o / l);
    n = l / (u4)r;
    m = (unsigned char)((u4)o / n);
  }
  d = (unsigned char)(l + (u4)r);
  e = o;
  if (! (a % (unsigned int)m)) {
    d = (unsigned char)(l - (u4)m);
    e = (unsigned char)((u4)o + l);
  }
  else 
    if (a % (unsigned int)m == (unsigned int)r) {
      d = (unsigned char)l;
      e = (unsigned char)(n + (u4)o);
    }
  *(t + k) = d;
  *(t + r) = e;
  *u = d;
  memcpy((void *)c,(void const *)t,(unsigned long)b);
  __retres = c + b;
  return __retres;
}

void K(u1 *c, u4 a)
{
  u1 *b;
  u1 *d;
  u2 e;
  u2 f;
  u4 g;
  u4 h;
  u4 i;
  u4 j;
  u2 tmp;
  u4 tmp_0;
  u4 tmp_1;
  u4 tmp_2;
  u1 tmp_3;
  u4 tmp_5;
  u1 tmp_4;
  u1 tmp_6;
  u1 tmp_7;
  u1 *tmp_8;
  u1 *tmp_9;
  u1 *tmp_10;
  int tmp_11;
  u1 *tmp_12;
  u1 *tmp_13;
  u4 tmp_14;
  u1 *tmp_15;
  u1 *tmp_16;
  u1 *tmp_17;
  u1 *tmp_18;
  u4 tmp_19;
  o = (unsigned char)(n ^ k);
  m = (unsigned char)l;
  l = (unsigned int)((int)o << (int)o);
  f = A((c + l) + (int)o);
  tmp = A(((c + l) + (int)o) + (int)o);
  tmp_0 = k;
  k -= (u4)1;
  e = (unsigned short)((int)tmp >> tmp_0);
  tmp_1 = k;
  k += (u4)1;
  p = (unsigned char)(~ tmp_1);
  tmp_2 = k;
  k -= (u4)1;
  p = (unsigned char)((int)p >> tmp_2);
  q = (unsigned char)((int)p >> n);
  tmp_3 = q;
  q = (unsigned char)((int)q - 1);
  ;
  if ((int)e >> (int)tmp_3) exit((int)(n + (u4)o));
  ;
  tmp_4 = q;
  q = (unsigned char)((int)q - 1);
  ;
  tmp_5 = I(c + (int)tmp_4,(unsigned int)f);
  g = tmp_5 / (u4)e;
  tmp_6 = D((unsigned int)e);
  i = (n + (u4)o) + (u4)tmp_6;
  t = (u1 *)malloc((unsigned long)i);
  if (! t) exit((int)(n * (u4)o));
  j = g * i + (u4)q;
  b = (u1 *)malloc((unsigned long)j);
  l -= (u4)1;
  r = (unsigned char)l;
  l += (u4)1;
  if (! b) exit((int)r);
  *b = (unsigned char)((l << n) | (unsigned int)q);
  *(b + ! k) = (unsigned char)((int)*b + (int)r);
  *(b + n) = (unsigned char)((u4)((int)*b << n) + n);
  tmp_7 = r;
  r = (unsigned char)((int)r - 1);
  *(b + o) = (unsigned char)((int)*(b + n) + (int)tmp_7);
  B(b + n * (u4)o,(unsigned short)(j - l));
  B(b + (int)o * (int)o,(unsigned short)((j - l) >> (u4)o * l));
  d = t;
  tmp_8 = d;
  d ++;
  *tmp_8 = (unsigned char)k;
  tmp_9 = d;
  d ++;
  *tmp_9 = (unsigned char)((int)r * (int)r);
  m = (unsigned char)((u4)p / (n + (u4)o));
  tmp_10 = d;
  d ++;
  *tmp_10 = (unsigned char)(((int)p - (int)m) - (int)o);
  tmp_11 = F((unsigned int)e,d);
  d += tmp_11;
  u = d;
  tmp_12 = d;
  d ++;
  *tmp_12 = (unsigned char)((int)r * (int)r);
  *d = (unsigned char)k;
  d = b + l;
  tmp_13 = d;
  d ++;
  tmp_14 = k;
  k += (u4)1;
  *tmp_13 = (unsigned char)tmp_14;
  tmp_15 = d;
  d ++;
  *tmp_15 = (unsigned char)(((int)p + (int)q) + (int)q);
  memcpy((void *)d,(void const *)(t + k),(unsigned long)(i - k));
  d += i - k;
  h = k;
  while (h < g) {
    d = J(d,h,i);
    h += (u4)1;
  }
  l = (unsigned int)(((int)o + (int)m) / (int)s - (int)m);
  o = r;
  tmp_16 = d;
  d ++;
  k -= (u4)1;
  *tmp_16 = (unsigned char)k;
  tmp_17 = d;
  d ++;
  *tmp_17 = (unsigned char)(~ k);
  tmp_18 = d;
  d ++;
  *tmp_18 = (unsigned char)((u4)((int)p / (int)o) - (u4)o * l);
  tmp_19 = k;
  k += (u4)1;
  *d = (unsigned char)tmp_19;
  *(c + (l + (u4)p)) = (unsigned char)k;
  B((c + l) + (int)o,(unsigned short)((u4)f + k));
  fwrite((void const *)c,(unsigned long)a,(unsigned long)(! (! c)),
         __fc_stdout);
  fwrite((void const *)b,(unsigned long)j,(unsigned long)(! (! b)),
         __fc_stdout);
  return;
}

int main(void)
{
  int __retres;
  u4 a;
  u4 b;
  u1 *c;
  size_t tmp;
  k = (unsigned int)(! (! __fc_stdin));
  n = (k + k) + k;
  l = k << n;
  m = (unsigned char)l;
  l = (l | (l >> (k + k))) << k;
  b = k << l;
  c = (u1 *)malloc((unsigned long)b);
  if (! c) exit((int)m);
  tmp = fread((void *)c,(unsigned long)k,(unsigned long)b,__fc_stdin);
  a = (unsigned int)tmp;
  l = (u4)(((int)m << k) + (int)m) + k;
  if (a >= b) exit((int)(l / n + k));
  if ((u4)*(c + n) != l << (k + k)) exit((int)((u4)((int)m << k) - (n << k)));
  else 
    if ((u4)*(c + ((u4)m - k)) != n + n) exit((int)((u4)((int)m << k) - (
                                                    n << k)));
  K(c,a);
  __retres = ! b;
  return __retres;
}