Download center

The licensing terms for Frama-C, the GNU LGPL v2, allow it to be used by all developers, including those developing proprietary software, without any license fees or royalties.

Support and Documentation

Helium version

Beryllium version Latest version Hydrogen version

Frama-C Helium [Changes]

20080701Source distribution [Compilation instructions]
20080701 Windows binary installer
20080701 ACSL 1.3 (Helium implementation)

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