Contact

If you think Frama-C could be part of any kind of scientific collaboration, including research projects, internships, PhDs, post-doctoral positions and dissemination activities, please contact:

Benjamin Monate Loïc Correnson

Authors

The Frama-C platform is co-developed by two French public institutions:

CEA–LIST (Software Reliability Laboratory) INRIA-Saclay (ProVal project)

Credits

Frama-C is supported by several collaborative projects :

OpenTC (Open Trusted Computing).
This project is cofinanced by the European Commission through the IST/FP6/IP programme.
CAT (C analysis toolbox).
This RNTL research project is funded by the ANR (French National Research Agency).
€-Confidential.
This is an EUREKA/ITEA European Research Programme.

static int x = 1; static long mc1[8][8], mc2[8][8]; /* if (init) { for (;;) } (long m1[8][8], long m2[8][8]) { long i, j, k, tmp1[8][8], tmp2[8][8]; /* Loops indexes and temporary matrices. */ double ftmp1, ftmp2; static int init = 1; static long mc1[8][8], mc2[8][8]; /* hard-coded cosines matrices. */if (init) { for (i = 0; i < 8; i++) for (j = 0; j < 8; j++) { ftmp1 = ((j == 0) ? 0; static long mc1[8][8], mc2[8][8]; /* hard-coded cosines matrices. */if (init) { for (i = 0; i < 8; i++) for (j = 0; j < 8; j++) { ftmp1 = ((j == 0) ? 0.5 / sqrt (2.0) : 0.5) * cos ((2.0 * i + 1.0) * j * TH); ftmp2 = ftmp1; /* The well known formula. The max absolute value for ftmp1 and ftmp2 is 0.5. */ ftmp1 *= (1 << NBC1); if (ftmp1 < 0) ftmp1 -= 0.5; else ftmp1 += 0.5; mc1[i][j] = ftmp1; ftmp2 *= (1 << NBC2); /* Multiply the cosine coefficient by 2^NBC2. The max absolute value for * ftmp2 is 2^(NBC2-1). */ if (ftmp2 < 0) ftmp2 –= 0.5; else ftmp2 += 0.5; /* For symetrical rounding. */ mc2[i][j] = ftmp2; } init = 0; } /* Then the first pass. */ for(i = 0; i < 8; i++) for(j = 0; j < 8; j++) { for(k = 0, tmp1[i][j] = 0; k < 8; k++)tmp1[i][j] += mc1[i][k] * m1[k][j]; /* The [i,j] coefficient of the matrix product MC1*M1. */ tmp1[i][j] >>= (NBC1 + 10 – NBI); tmp1[i][j] += 1; /* For rounding purpose. */ tmp1[i][j] >>= 1; /* Final rounding. tmp1[i][j] is now represented on NBI bits. */if (tmp1[i][j] < -(1 <<