This directory contains version of external programs that allows to compile the Cost frama-c plugin (the Nitrogen version) and to run the tests.

experiments/frama-c_plugin/trunk/Nitrogen/
experiments/frama-c_plugin/trunk/Nitrogen/plugin/tests

All the programs are installed in the local usr directory in this directory.


The instructions for frama-c why3 why2 (in this order):
- export PATH=$PWD/usr/bin:$PATH  (do that in the directory of this readme)
- untar with "tar -xjf" to uncompress the archive in their own directory
- run autoconf if needed
- frama-c why2: ./configure --prefix=$PWD/../../usr  (and install all the needed library)
- why3: ./configure --enable-local
- make
- make install

Then:
- make -C why3/why test-runstrat.opt

Detect the provers:
- why3config

Go in experiments/compiler/trunk/8051:
- ./configure --prefix ../../../external_programs/usr
- make
- make install

Go in experiments/frama-c_plugin/trunk/Nitrogen:
- Don't forget "experiments/external_programs/usr/bin" must be in the path
- ./configure --prefix $PWD/../../../external_programs/usr
- make
- make install

Go in experiments/frama-c_plugin/trunk/Nitrogen/plugin/tests/success:
- make -k -j 4 (other your number of processor)
- make showresult