- 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
