User Tools

  • Logged in as: anonymous (anonymous)
  • Logout

Site Tools


mantis:frama-c:faq

Tips and Frequently asked questions

Frequently Asked in frama-c-discuss

Éric Jenn has compiled a list of Frequently Asked Questions and answers based on contributions to the frama-c-discuss list.

Parsing

Pre-processing the annotations

By default, the preprocessor does not process comments. ACSL annotations, unfortunately, look like comments to the preprocessor. If you use the GCC preprocessor (also known as GNU CPP), you can force the preprocessing of annotations with the -pp-annot option.

frama-c -pp-annot [other options]

Using standard headers

Since Frama-C Boron, a large part of the C99 standard library headers are installed with Frama-C, in the ${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]

Booleans

The C99 type bool is not automatically 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.

What do I need to be able to use the Windows Frama-C package?

You need to install a C preprocessor. Any preprocessor can be used, but the best preprocessor to choose is the one that is supposed to be used to preprocess the application you want to analyze.

If you just seek any C preprocessor for testing purpose, you may want to install Cygwin and add the gcc development package or any version you can find on the web. Page 40 of the Value analysis manual gives hints for other preprocessors (MSVC):

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’

Jessie and WP

Installing theorem provers

Links for installing provers are provided on Why3's page.
Here are detailed instructions for making use of Z3:

  • Click on the 'Download' button
  • Save the zip in a local folder, say z3-sources/.
  • Run the following commands:
cd z3-sources
unzip z3[tab for completion]
cd z3[tab for completion]
autoconf
./configure
python scripts/mk_make.py
cd build
make
sudo make install
  • z3 executable is installed at /usr/bin, libraries at /usr/lib, and include files at /usr/include.
  • Run why3config –detect (the provers, the versions and the plugins detected can be differrent)
Found prover Alt-Ergo version 0.95.1, Ok.
Found prover CVC3 version 2.4.1, Ok.
Found prover Spass version 3.7, Ok.
Found prover Z3 version 4.3.1, Ok.
Found prover Coq version 8.4pl1, Ok.
Warning: prover Gappa version 0.17.1 is not known to be supported, use it at your own risk!
5 provers detected and 1 provers detected with unsupported version
== Found [..]/why3/lib/why3/plugins/hypothesis_selection.cmxs ==
== Found [..]/why3/lib/why3/plugins/tptp.cmxs ==
== Found [..]/why3/lib/why3/plugins/dimacs.cmxs ==
== Found [..]/why3/lib/why3/plugins/genequlin.cmxs ==
Save config to ~/.why3.conf

Jessie specific questions

Graphical user interface

Is there an Eclipse plug-in?

  • An Eclipse plug-in providing equivalent functionality to gWhy (for Weakest Precondition plug-ins) is currently maintained by Nickolay V. Shmyrev and is available on GitHub. This plug-in works on Linux, but not yet on Windows.
  • fcdt is another Eclipse plug-in, that allows to use value analysis from Eclipse

How do I customize the GUI?

Starting with 20090901 (Beryllium), you can create a file named frama-c-user.rc in $FRAMAC_SHARE. An example of the syntax to use can be found in the file $FRAMAC_SHARE/frama-c.rc.

Misc

Validity of memory zones

ACSL (hence Frama-C) 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 code below is correct

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

Checking the alignment of some memory accesses with the value analysis

It is possible to check explicitly that a few memory accesses are aligned with the value analysis. Check the Explicit alignment howto.

mantis/frama-c/faq.txt · Last modified: 2013/05/21 17:01 by bobot