Documentation pages

dokuwiki/faq.md

----
-layout: clean_page
----
-# Tips and Frequently asked questions
-
-### Frequently Asked in frama-c-discuss
-
-Éric Jenn has compiled a list of [Frequently Asked Questions](/dokuwiki/frequently_asked_questions.html) and answers based on
-contributions to the
-[frama-c-discuss](/mailto/frama-c-discuss@lists.gforge.inria.fr) 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](http://why3.lri.fr/#provers).  
-Here are detailed instructions for making use of Z3:
-
-  - go to [Z3 source
-    homepage](http://z3.codeplex.com/SourceControl/latest#README)
-  - Click on the 'Download' button
-  - Save the zip in a local folder, say z3-sources/.
-  - Run the following commands:
-
-<!-- end list -->
-
-    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)
-
-<!-- end list -->
-
-    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
-
-See [Jessie's page](/dokuwiki/jessie.html).
-
-# 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 [[http://github.com/frama-c-eclipse/frama-c-eclipse|is available on GitHub]]. This plug-in works on Linux, but not yet on Windows.
-  * (fcdt)[http://gforge.enseeiht.fr/projects/fcdt/|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](Explicit%20alignment%20howto).