Forked from
pub / open-source-case-studies
204 commits behind the upstream repository.
-
Andre Maroneze authoredAndre Maroneze authored
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;
}