Is on-topic in this wiki anything that may be of help to others users of Frama-C and related tools: tips, changes that you have noticed, workarounds, etc. If it should have been in the manual, put it here. If it's too minute, platform-specific, or temporary to be a good fit for the manual, put it here. Your goal should be to make a wiki so clear and functional that it puts the authors of Frama-C's various manuals to shame.
Do not be afraid to reorganize the words of others if you feel that makes the wiki more useful as a whole. They agreed to let you do that when they chose to participate, and so do you.
This site contains all possible syntax you may use when editing the pages of this wiki. This wiki is moderated after-the-fact.
env MAKE=gmake bash ./configure CFLAGS=”-I/usr/local/include”
LDFLAGS=”-L/usr/local/lib” && gmake
* How can I compile the Jessie plugin coming with Why 2.22 under Windows?
C:\Frama-C\bin to PATHOCAMLLIB to C:\Frama-C\libCAML_LD_LIBRARY_PATH to C:\Frama-C\lib\stublibs C:\Frama-C by your installation path if you customized it.gcc-mingw and autoconf packagesC:\Cygwin\bin\gcc.exe is a symbolic link, remove it and replace it by its full expansion e.g. gcc-3.exe under Cygwin 1.7 beta../configure –prefix C:/Frama-C (forward slash must be used!)makemake FRAMAC_LIBDIR=“C:\\\Frama-C\\\lib\\\frama-c” install (triple backward slashes must be used!)frama-c-gui -cpp-command ’gcc -C -E -I . -x c ’ frama-c-gui -cpp-command ’gcc -C -E -I . -o %2 %1' frama-c-gui -cpp-command ’copy %1 %2’ frama-c-gui -cpp-command ’cat %1 > %2’ frama-c-gui -cpp-command ’CL.exe /C /E %1 > %2’
$HOME/bin directory.bashrc add:export PATH=$HOME/bin:$PATH$HOME/bin add file z3 with contentargs=`echo $* | sed -e 's|/|\\\|g'` exec wine $HOME/.wine/drive_c/Program_Files/Microsoft_Research/Z3-1.3.6/bin/z3.exe /s $argssudo chmod 775 z3why-configstarting autodetection... Found prover Alt-Ergo version 0.8 Found prover Simplify version 1.5.4 err:winedevice:ServiceMain driver L"vstor2-ws60" failed to load Found prover Z3 version 1.3 Found prover Yices version 1.0.21 Found prover CVC3 version devel Found prover Coq version 8.1pl3 detection done. writing rc file...
Frama-C/Jessie uses a typed memory model. That is, each block of allocated memory is associated with a type. These can be simple types, such as char or int, as well as structs. Therefore, the following verifies with Jessie:
struct A {
int x;
int y;
};
struct B {
struct A a;
int z;
};
/*@ requires \valid(p);
*/
void foo(struct B *p) {
p->a.x = 0;
p->z = 0;
}
Note however that arrays are considered as chunks of data of the same type. Therefore, this example does not verify:
typedef int arr3[3];
/*@ requires \valid(a);
*/
foo(arr3 a) {
a[2] = 0;
}
Instead, the correct annotation is
typedef int arr3[3];
/*@ requires \valid(a+ (0..2));
*/
foo(arr3 a) {
a[2] = 0;
}
The C99 type bool is not supported by Frama-C. To use bool in your code, add this line:
typedef enum _bool { false = 0, true = 1 } bool ;
Note that C99 uses a pre-defined type _Bool (see paragraph 6.2.5), that is supported by Frama-C. The standard library defines a macro bool (that expands to _Bool) in stdbool.h. Since Frama-C Boron, this header file can be found in ${FRAMAC_SHARE}/libc. See below to understand how such headers can be included in your code.
-pp-annot option.usage: extract_obligation -f=funname -o=obligation [-s=solver] sources
Options:
-s=<solver> or --solver=<solver> with solver in {coq,smtlib,alt-ergo} (default is coq)
-f=<fun> or --function=<fun> with fun a function in sources
-o=<obl> or --obligation=<obl> with obl an obligation associated to the function (the name in available in the frama-c gui with jessie plugin)\\
${FRAMAC_SHARE}/libc directory. It is better to use these headers rather than the ones that might be present on your system, as they contain some specific information that will help the analyses, such as in particular ACSL specifications for some of the functions. In order to #include such an header file, you can use e.g. the following command:frama-c -cpp-extra-args="-I`frama-c -print-path`/libc" [other options]
There is a list of publications related to Frama-C.