Community Support

Several public support options are available:

The Stack Overflow website, where questions should be labeled with the frama-c tag. There also exists a general discussion list.
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.
The Frama-C blog will keep you informed on what is going on within Frama-C.

For any question about Frama-C, of if you are looking for any collaboration (academic or industrial) with us, please contact: support@frama-c.com.

Download Center

Documentation

Manuals and tutorials

ACSL Specification Language

Frama-C Platform

Plug-ins

A short description of each plug-in can be found into the Plug-in Factory.
Direct links to each plug-in's full documentation are listed below:

Other material

A list of publications related to Frama-C is maintained on the wiki.
A list of available positions for working on Frama-C is maintained on the wiki.
Frama-C's blog
Slides and code examples from the Frama-C training workshop held on October 2010 in Berlin.
draft version of the ISO C99 standard.

External Resources

(in French) Atos Formation includes 2 training courses on Frama-C in its offer.

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–2012 Terms of Use