Community Support

Two public support options are available:

The general discussion list on the Frama-C platform
The bug tracking system. To submit a new bug, you must open an account on the bts.
The Frama-C wiki is accessible. To edit it, you must open an account on the bts.

For any question about Frama-C, of if you are looking for any collaboration (academic or industrial) with us, please contact: Benjamin Monate, Loïc Correnson.

Download Center

Documentation

ACSL Specification Language

Frama-C Platform

Plug-ins Quick Links

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 <<

© CEA–LIST 2007–2009 Terms of Use