### Frama-C and Why Installation Guide Source: https://frama-c.com/html/fc-discuss/2010-June/msg00016 Provides shell commands for compiling and installing Frama-C and the Why tool. It outlines the steps: configuring, compiling, and installing both components separately, and emphasizes ensuring Frama-C is in the PATH for Why to detect it. This guide is intended for manual installation from source. ```shell cd why ./configure make make install (may require superuser right) ``` -------------------------------- ### Setup Why3 and Alt-Ergo Provers with Opam Source: https://frama-c.com/html/fc-discuss/2020-September/msg00004 This section details the installation of Why3, its IDE, and the Alt-Ergo prover using Opam. It also includes system dependency installations required for these tools. ```bash sudo apt-get install libgmp-dev libgtksourceview2.0-dev m4 opam install why3 why3-ide alt-ergo ``` -------------------------------- ### Compile and Install APRON Library Source: https://frama-c.com/html/fc-discuss/2009-March/msg00000 Downloads, compiles, and installs the APRON analysis library. It configures the installation prefix and includes necessary development packages like libgmp3-dev and camlidl. ```shell $ wget http://apron.cri.ensmp.fr/library/apron-0.9.9.tgz $ tar zxf apron-0.9.9.tgz $ cd apron-0.9.9 # aptitude install libgmp3-dev libmpfr-dev # aptitude install camlidl $ cp Makefile.config.model Makefile.config -- Makefile.config.model 2008-06-09 16:10:50.000000000 +0200 +++ Makefile.config 2009-02-27 09:54:44.000000000 +0100 @@ -29,7 +29,7 @@ # Where to install and to find APRON # ($(APRON_PREFIX)/include, $(APRON_PREFIX)/lib) # -APRON_PREFIX = /usr +APRON_PREFIX = /usr/local/stow/apron-0.9.9 # Where to install and to find MLGMPIDL # ($(MLGMPIDL_PREFIX)/lib) $ make $ make install $ cd /usr/local/stow/ $ stow apron-0.9.9 ``` -------------------------------- ### Install Frama-C on Windows (WSL) using opam Source: https://frama-c.com/html/get-frama-c Installs Frama-C within Windows Subsystem for Linux (WSL) by preparing opam, installing graphical dependencies like lablgtk3, and then installing Frama-C. This method includes setting up opam without sandboxing and enabling depext for dependency resolution. The GUI can be launched with a specific backend. ```shell # 1. Prepare opam installation sudo apt update && sudo apt upgrade sudo apt install make m4 gcc opam # 2. opam setup opam init --disable-sandboxing --shell-setup eval $(opam env) opam install -y opam-depext # 3. Install graphical dependencies opam depext --install -y lablgtk3 lablgtk3-sourceview3 # 4. Install Frama-C opam depext --install -y frama-c # On WSL2, run the GUI as: GDK_BACKEND=x11 frama-c-gui ``` -------------------------------- ### Compile and Install Alt-Ergo Prover Source: https://frama-c.com/html/fc-discuss/2009-March/msg00000 Downloads, compiles, and installs the Alt-Ergo prover (version 0.8). It uses stow for managing the installation prefix and includes dependency installation for ocamlgraph. ```shell $ wget http://alt-ergo.lri.fr/http/alt-ergo-0.8.tar.gz $ tar zxf alt-ergo-0.8.tar.gz $ cd alt-ergo-0.8 # aptitude install libocamlgraph-ocaml-dev $ ./configure --prefix=/usr/local/stow/alt-ergo-0.8 $ make $ make install $ mkdir /usr/local/stow/alt-ergo-0.8/bin $ make install $ cd /usr/local/stow/ $ stow alt-ergo-0.8 ``` -------------------------------- ### Install OCaml Dependencies for Frama-C Source: https://frama-c.com/html/fc-discuss/2009-March/msg00000 Installs essential OCaml development libraries and compilers required for Frama-C and its associated tools on Debian systems using aptitude. ```shell # aptitude install liblablgtk2-gnome-ocaml-dev \ liblablgtksourceview-ocaml-dev liblablgtk2-ocaml-dev ocaml \ ocaml-native-compilers ocaml-mode \ stow ``` -------------------------------- ### Frama-C Execution Output Example Source: https://frama-c.com/html/fc-discuss/2009-July/msg00031 This output shows the result of running Frama-C on a C code file. It includes the preprocessing step, parsing, cleaning unused parts, symbolic link creation, and the start of semantic analysis. ```shell frama-c a.c [kernel...] preprocessing with "gcc -C -E -I. ? a.c" Here is my output with Frama-C Beryllium-beta1: $ frama-c -version Version: Beryllium-20090601-beta1 Compilation date: Thu Jul 23 11:12:28 CEST 2009 Share path: /usr/local/share/frama-c (may be overridden with FRAMAC_SHARE variable) Library path: /usr/local/lib/frama-c Plug-in paths: /usr/local/lib/frama-c/plugins (may be overriden with FRAMAC_PLUGIN variable) $ frama-c a.c [kernel...] preprocessing with "gcc -C -E -I. ? a.c" Here is my output with Frama-C Lithium: $ frama-c -version ./bin/toplevel.opt -version Version: Lithium-20081201 Compilation date: Mon May 4 18:22:12 CEST 2009 Frama-C library path: /usr/local/share/frama-c (may be overridden with FRAMAC_SHARE variable) Parsing Cleaning unused parts Symbolic link Starting semantical analysis $ frama-c a.c Parsing [preprocessing] running gcc -C -E -I. ? a.c Cleaning unused parts Symbolic link Starting semantical analysis ``` -------------------------------- ### Frama-C Dynamic Plugin Makefile Example Source: https://frama-c.com/html/fc-discuss/2012-July/msg00051 This Makefile snippet is used for building and installing dynamic plugins for Frama-C. It demonstrates how to specify plugin directories and names, and includes Frama-C's Makefile.dynamic. It requires Frama-C to be installed. ```makefile # Frama-c should be properly installed with "make install" # before any use of this makefile FRAMAC_SHARE :=$(shell frama-c.byte -print-path) FRAMAC_LIBDIR :=$(shell frama-c.byte -print-libpath) PLUGIN_DIR ?= . PLUGIN_NAME := MyPlugin PLUGIN_CMI := PLUGIN_CMO := register include $(FRAMAC_SHARE)/Makefile.dynamic ``` -------------------------------- ### Frama-C Command for Jessie Analysis Source: https://frama-c.com/html/fc-discuss/2010-September/msg00011 Example command to run Frama-C with the Jessie plugin for static analysis on a C file named 'swap1.c'. This command utilizes the 'simplify' option and aims to generate verification conditions for the 'swap' function. ```bash frama-c -jessie -jessie-atp simplify swap1.c ``` -------------------------------- ### Frama-C Installation Problem and Analysis Output (Shell) Source: https://frama-c.com/html/fc-discuss/2009-January/msg00006 Demonstrates a Frama-C installation issue related to finding the 'prelude.why' file during analysis. It shows environment variable setup, the command executed, and the resulting error message from the 'make' utility. This snippet is relevant for diagnosing build and analysis problems in Frama-C. ```shell WHYLIB=C:\\cygwin\\usr\\local\\Frama-C\\share\\frama-c\\why frama-c -jessie-analysis -jessie-gui a.c Parsing [preprocessing] running gcc -C -E -I. -include /usr/local/share/frama-c\jessie\jessie_prolog.h -dD a.c Cleaning unused parts Symbolic link Starting semantical analysis Starting Jessie translation Producing Jessie files in subdir a.jessie File a.jessie/a.jc written. File a.jessie/a.cloc written. Calling Jessie tool in subdir a.jessie Generating Why function max Calling VCs generator. gwhy-bin [...] why/a.why cannot find prelude file /usr/local/share/frama-c/why\why\prelude.why make: *** [a.stat] Error 1 Jessie subprocess failed: make -f a.makefile gui ``` -------------------------------- ### Install Frama-C on Mac using OPAM Source: https://frama-c.com/html/fc-discuss/2013-April/msg00025 This snippet details the steps to install Frama-C on a Mac using the OPAM package manager. It includes installing necessary ports, initializing OPAM, setting up an environment switch, and installing Frama-C itself. It also covers installing the Jessie plugin, which may include other heavy dependencies like Coq. ```shell port install opam port install gtksourceview2 opam init eval `opam config env` opam switch 4.00.1 opam install frama-c opam install why ``` -------------------------------- ### Install Frama-C Jessie Plugin using OPAM Source: https://frama-c.com/html/fc-discuss/2013-April/msg00024 This snippet demonstrates how to install the Jessie plugin for Frama-C after the initial Frama-C installation. It highlights that this process also installs other tools like why3, coq, and alt-ergo, which can be time-consuming. ```bash opam install why ``` -------------------------------- ### Install Frama-C and Dependencies using OPAM Source: https://frama-c.com/html/fc-discuss/2017-June/msg00007 This section provides a step-by-step guide to install Frama-C and its dependencies using OPAM, emphasizing the uninstallation of conflicting Ubuntu OCaml packages. It ensures proper setup for Frama-C GUI functionality. ```shell ./opam_installer.sh BINDIR 4.02.3 opam install depext opam depext frama-c opam install frama-c ``` -------------------------------- ### Install Frama-C on Linux using opam Source: https://frama-c.com/html/get-frama-c Installs Frama-C on Linux systems by first installing the opam package manager, initializing it with an OCaml compiler, and then installing Frama-C and its dependencies. This method may require sudo privileges for installing system dependencies. ```shell # 1. Install opam (OCaml package manager) sudo apt install opam # or dnf, pacman, etc. # Or you can download an opam binary, put it in the PATH # and run it directly (no sudo required) # 2. Initialize opam (install an OCaml compiler) opam init --compiler 4.14.1 # may take a while eval $(opam env) # 3. Install Frama-C (including dependencies) opam install frama-c # opam will install system package dependencies; # may require sudo ``` -------------------------------- ### Using Frama-C with Why3 and Jessie Plugin Source: https://frama-c.com/html/fc-discuss/2012-July/msg00039 Instructions on how to set up and use Frama-C with the Why3 platform and the Jessie plugin. This involves compiling Frama-C and Why3, then using the `why3config --detect` command to identify provers. Finally, the command `frama-c -jessie file.c` is used to start value set computations and the Why3 GUI. ```bash # compile and install Frama-C Nitrogen and Why3 in any order # compile and install Why 2.31 which contains the Jessie plugin # detect provers: why3config --detect frama-c -jessie file.c ``` -------------------------------- ### Install Frama-C on macOS using opam Source: https://frama-c.com/html/get-frama-c Installs Frama-C on macOS using Homebrew to manage dependencies like opam and gmp, followed by opam initialization and Frama-C installation. This approach leverages Homebrew for package management before proceeding with opam. ```shell # 1. Install Homebrew # 2. Install required dependencies for Frama-C brew install opam gmp # 3. Install recommended dependencies for Frama-C brew install graphviz zmq # 4. Initialize opam (install an OCaml compiler) opam init --compiler 4.14.1 # may take a while eval $(opam env) # 5. Finally install Frama-C opam install frama-c ``` -------------------------------- ### Frama-C Installation Commands Source: https://frama-c.com/html/fc-discuss/2010-June/msg00014 This snippet shows the standard commands for configuring, building, and installing Frama-C from source. It includes steps for the main Frama-C installation and a subdirectory 'why'. Dependencies include standard build tools like `make` and potentially superuser privileges for installation. ```shell ./configure make make install (may require superuser right) cd why ./configure make make install (may require superuser right) ``` -------------------------------- ### Running Frama-C with Jessie Plugin Source: https://frama-c.com/html/fc-discuss/2010-April/msg00033 Demonstrates running Frama-C with the Jessie plugin to analyze a C code snippet. It shows the preprocessing steps, plugin initialization, and potential errors like unsupported variadic functions. The example C code is a simple 'hello world' program. ```bash rtl26:~/formal_methods/Frama-C/examples# frama-c.byte -jessie hello.c [kernel] preprocessing with "gcc -C -E -I. -dD hello.c" [jessie] Starting Jessie translation [kernel] No code for function printf, default assigns generated hello.c:5:[jessie] failure: unsupported variadic functions [jessie] warning: Unsupported feature(s). Jessie plugin can not be used on your code. ``` -------------------------------- ### Install and Use Frama-C with Why3 and Jessie Plugin Source: https://frama-c.com/html/fc-discuss/2012-July/msg00038 Instructions for compiling and installing Frama-C Nitrogen and Why3, followed by the installation of the Why 2.31 package containing the Jessie plugin. It details how to detect provers and then use the frama-c command with the -jessie flag to compute VCs and launch the Why3 GUI. ```shell Compile and install Frama-C Nitrogen and Why3 (newer Why3 0.73 recommended if possible) Compile and install Why 2.31 which contains the Jessie plugin Detect provers: why3config --detect then: frama-c -jessie file.c ``` -------------------------------- ### Install Frama-C Dependencies with Homebrew Source: https://frama-c.com/html/fc-discuss/2011-November/msg00036 Commands to update Homebrew repositories and install essential dependencies (atk, glib, pango, cairo, gdk-pixbuf) that are often required for building software like Frama-C on macOS. ```bash brew update brew install atk glib pango cairo gdk-pixbuf ``` -------------------------------- ### Frama-C Installation Commands Source: https://frama-c.com/html/fc-discuss/2014-September/msg00024 These commands illustrate the installation process for Frama-C, Why3, and Alt-Ergo on a Windows machine using Cygwin. The commands include 'configure', 'make', and 'make install' for Frama-C and Why3, and downloading a pre-compiled binary for Alt-Ergo. ```bash # Frama-C Neon installation ./configure & make & make-install. $ which frama-c /usr/bin/frama-c ``` ```bash # Why3 installation ./configure make make install $which why3 /usr/bin/why3 ``` ```bash # Alt-Ergo installation (using pre-compiled binary) $ which alt-ergo /usr/bin/alt-ergo ``` -------------------------------- ### Install Frama-C and Provers using Opam Source: https://frama-c.com/html/fc-discuss/2020-September/msg00006 This snippet demonstrates the installation process for Frama-C and associated provers (alt-ergo, why3) using the opam package manager. It includes steps for initializing opam, installing dependencies, pinning CoqIDE, and configuring the 'why3' tool. This is applicable to Ubuntu and macOS environments. ```shell opam init --yes --comp=4.09.1 opam install --yes depext opam depext --yes frama-c opam pin add --yes coqide 8.9.1 opam install --yes frama-c alt-ergo why3 why3-coq why3 config --full-config ``` -------------------------------- ### Configure Script Summary - System Dependencies Source: https://frama-c.com/html/fc-discuss/2017-August/msg00033 This summary provides a clear overview of the system configuration for Frama-C. It lists the detected versions of OCaml, Frama-C, and Why3, along with the status of support for other provers and plugins. ```text Summary ----------------------------------------- OCaml version : 4.03.0 OCaml library path : /Users/david/.opam/4.03.0/lib/ocaml OcamlGraph lib : found by ocamlfind Verbose make : no Inference of annotations : no Why3 support : yes Binary : /Users/david/.opam/4.03.0/bin/why3 Version : unknown version , hope this works Frama-C plugin : yes Binary : /Users/david/.opam/4.03.0/bin/frama-c Version : Silicon-20161101 Coq support (via Why3) : no command 'coqc' not found PVS support (via Why3) : no command 'pvs' not found Other provers support : (via Why3) ``` -------------------------------- ### Compile and Install CCVC3 Prover with GCC 4.3 Patch Source: https://frama-c.com/html/fc-discuss/2009-March/msg00000 Compiles and installs the CCVC3 prover (version 1.5), including a necessary patch for compatibility with GCC 4.3.x. The installation is managed using stow. ```shell $ wget http://www.cs.nyu.edu/acsys/cvc3/download/1.5/cvc3-1.5.tar.gz $ tar zxf cvc3-1.5.tar.gz $ cd cvc3-1.5 $ ./configure --prefix=/usr/local/stow/cvc3-1.5 --disable-zchaff Apply following patch for GCC 4.3.x: === patch begin === diff -ur /tmp/cvc3-1.5/src/include/command_line_flags.h ./include/command_line_flags.h --- /tmp/cvc3-1.5/src/include/command_line_flags.h 2006-08-09 23:19:30.000000000 +0200 +++ ./include/command_line_flags.h 2009-02-27 13:34:05.000000000 +0100 @@ -24,6 +24,7 @@ #include #include #include +#include #include "command_line_exception.h" #include "debug.h" diff -ur /tmp/cvc3-1.5/src/include/memory_manager.h ./include/memory_manager.h --- /tmp/cvc3-1.5/src/include/memory_manager.h 2006-08-09 23:19:30.000000000 +0200 +++ ./include/memory_manager.h 2009-02-27 13:33:06.000000000 +0100 @@ -34,6 +34,8 @@ #ifndef _cvc3__memory_manager_h #define _cvc3__memory_manager_h +#include + namespace CVC3 { class MemoryManager { diff -ur /tmp/cvc3-1.5/src/util/debug.cpp ./util/debug.cpp --- /tmp/cvc3-1.5/src/util/debug.cpp 2007-06-27 06:35:44.000000000 +0200 +++ ./util/debug.cpp 2009-02-27 13:27:15.000000000 +0100 @@ -22,7 +22,7 @@ #include #include "debug.h" - +#include using namespace std; namespace CVC3 { diff -ur /tmp/cvc3-1.5/src/util/rational-gmp.cpp ./util/rational-gmp.cpp --- /tmp/cvc3-1.5/src/util/rational-gmp.cpp 2007-08-07 22:46:03.000000000 +0200 +++ ./util/rational-gmp.cpp 2009-02-27 13:30:21.000000000 +0100 @@ -24,6 +24,7 @@ #include "compat_hash_set.h" #include "rational.h" +#include #include #include === patch end === $ make $ make install $ cd /usr/local/stow/ $ stow cvc3-1.5 ``` -------------------------------- ### Compiling Frama-C and Why with Shell Commands Source: https://frama-c.com/html/fc-discuss/2010-April/msg00065 This snippet demonstrates the standard shell commands used for configuring, compiling, and installing software packages like Frama-C and Why. It involves running `./configure`, `make`, and `sudo make install` sequentially. These commands are essential for building software from source on Unix-like systems. ```shell ./configure make sudo make install ``` -------------------------------- ### Install Homebrew and Custom Frama-C Formulas Source: https://frama-c.com/html/fc-discuss/2011-November/msg00036 Instructions to install Homebrew using a Ruby script and then manually copy custom formula files for Frama-C and its dependencies (gtk-gnutella, frama-c, libgnomecanvas) from a GitHub repository to the local Homebrew formula directory. ```bash # Install Homebrew /usr/bin/ruby -e "$(curl -fsSL https://raw.github.com/gist/323731)" # Copy custom formula files cd /usr/local/Library/Formula/ sudo curl -O https://raw.github.com/ismaelvb/homebrew/890c894f26e826b71bc33c73bb1f5a4f393a0740/Library/Formula/gtk-gnutella.rb sudo curl -O https://raw.github.com/ismaelvb/homebrew/master/Library/Formula/frama-c.rb sudo curl -O https://raw.github.com/ismaelvb/homebrew/f0b08276fa4421adaee1b40c01065282306cb65a/Library/Formula/libgnomecanvas.rb ``` -------------------------------- ### Frama-C Analysis Command Example Source: https://frama-c.com/html/fc-discuss/2017-June/msg00005 An example command to launch Frama-C with verbose output for kernel and analysis options, as used in the neovim development context. ```bash ./frama.sh -verbose=40 -kernel-verbose=40 ``` -------------------------------- ### Install Homebrew and Frama-C Formulae on Mac Source: https://frama-c.com/html/fc-discuss/2011-November/msg00034 This script installs Homebrew, downloads custom formula files for Frama-C and its dependencies (gtk-gnutella, libgnomecanvas), and then installs Frama-C using Homebrew. It assumes a macOS environment with a terminal. The Homebrew installation command fetches a Ruby script. The subsequent `curl` commands download specific .rb files directly into the Homebrew Library/Formula directory. Finally, `brew install frama-c` compiles and installs the software. Linking is recommended for PATH availability. ```shell #!/bin/bash # Install Homebrew /usr/bin/ruby -e "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/master/install)" # Navigate to Homebrew's formula directory cd /usr/local/Library/Formula/ # Download Frama-C dependencies and Frama-C itself sudo curl -O https://raw.github.com/ismaelvb/homebrew/master/Library/Formula/gtk-gnutella.rb sudo curl -O https://raw.github.com/ismaelvb/homebrew/master/Library/Formula/frama-c.rb sudo curl -O https://raw.github.com/ismaelvb/homebrew/master/Library/Formula/libgnomecanvas.rb # Install Frama-C brew install frama-c # Link Frama-C to make it available in the PATH sudo brew link frama-c # Note: This script is intended for macOS (SL and Lion tested) and may require modifications for other versions or operating systems. ``` -------------------------------- ### Frama-C Jessie Prover Configuration Example Source: https://frama-c.com/html/fc-discuss/2013-September/msg00108 This example demonstrates Frama-C configuration settings used to prove loop invariants. It includes specifying prover commands, time limits, and specific plugins like Jessie. The example also shows how to modify annotations to be compatible with the Frama-C kernel and prover, such as replacing 'sum(x,...)' with 'sum(x+0,...)'. ```shell # Frama-C Fluorine 20130601 + Why 2.33 + Why3 + provers Alt-Ergo, CVC3 and Gappa. # Remove 'loop assigns p,j' to avoid disturbing Jessie. # Replace 'sum(x,...)' by 'sum(x+0,...)' to be accepted by Frama-C kernel. ``` -------------------------------- ### Frama-C Predicate Definition Example Source: https://frama-c.com/html/fc-discuss/2011-February/msg00047 This snippet demonstrates how to define a predicate in Frama-C for specifying properties of program locations. It includes an example of a predicate `bar_spec` and its usage in an `ensures` clause. This requires Frama-C to be installed and configured. ```C //@predicate bar_spec{L1,L2}(int * p) = \at(*p, L1) == at(*p, L1); //@ensures bar_spec{Here,Old}(&x) ; bar(); ``` -------------------------------- ### Compile and Test Frama-C Lithium Source: https://frama-c.com/html/fc-discuss/2009-March/msg00000 Compiles Frama-C Lithium, generates documentation, and runs its test suite. This snippet includes commands for configuring, building, and testing Frama-C, as well as sample output from a failed test case. ```shell # aptitude install coq coq-doc $ ./configure --prefix=/usr/local/stow/frama-c-lithium-2008-12-01 $ make $ make doc $ make ptests $ make oracles $ make tests Running ptests Command: ./bin/toplevel.opt -val -out -input -deps -journal-disable tests/jessie/minix3_strcpy.c 2>tests/jessie/result/minix3_strcpy.err.log >tests/jessie/result/minix3_strcpy.res.log --- tests/jessie/oracle/minix3_strcpy.err.oracle 2009-02-27 10:23:14.000000000 +0100 +++ tests/jessie/result/minix3_strcpy.err.log 2009-02-27 11:20:22.000000000 +0100 @@ -1,10 +1,10 @@ tests/jessie/minix3_strcpy.c:10:35: error: minix3_include/string.h: No such file or directory -Failed to run: gcc -C -E -I. -o '/tmp/minix3_strcpy.cd7b819.i' 'tests/jessie/minix3_strcpy.c' +Failed to run: gcc -C -E -I. -o '/tmp/minix3_strcpy.c8cbb0f.i' 'tests/jessie/minix3_strcpy.c' ``` -------------------------------- ### Troubleshooting Frama-C Command Not Recognized Source: https://frama-c.com/html/fc-discuss/2010-February/msg00031 This snippet provides commands to diagnose why the 'frama-c' command might not be recognized after installation on Mac OS X. It includes checking the current PATH environment variable and verifying the existence and type of the frama-c executable. These checks help in identifying issues with the installation path configuration. ```bash echo $PATH file /usr/local/Frama-C_Be/bin/frama-c ``` -------------------------------- ### CoqIDE environment setup Source: https://frama-c.com/html/fc-discuss/2010-February/msg00034 Command to launch CoqIDE with specific requirements, often used for debugging Coq code generation issues. It attempts to load necessary libraries like 'jessie_why'. ```bash $ coqide -require jessie_why framac_example.v ``` -------------------------------- ### Loop Invariant Example in Frama-C Discussion Source: https://frama-c.com/html/fc-discuss/2013-February/msg00014 This snippet shows an example of a loop invariant provided in a Frama-C discussion. It illustrates how to correctly define a loop invariant for a given code structure, focusing on the conditions that must hold true at the start and end of each iteration. The example is presented in a natural language context of an email exchange. ```text A better invariant (untested) would be \forall integer j; 0<=j G_E[j].G_Inst_Ativ <= Tempo ==> G_E[j].G_Ativo == 1; Notice how occurrences of i were replaced by j and how 0<=i<5 became 0<=j . 2) open with wine and install 3) create your home/user/bin directory 4) in .bashrc add : export PATH=/home/user/bin:$PATH 5) restart session 6)in home/user/bin add file z3 with content wine /home/dragan/.wine/drive_c/Program_Files/Microsoft_Research/Z3-1.3.6/bin/z3.exe /s $* 7)save and change permission 8)sudo chmod 775 z3 9) why-config ``` -------------------------------- ### Compiling Frama-C and Why Tool Source: https://frama-c.com/html/fc-discuss/2010-April/msg00064 This snippet demonstrates the standard compilation process for Frama-C and the Why tool using './configure', 'make', and 'sudo make install'. It also shows the manual copying of prover executables to the system's bin directory. ```shell ./configure make sudo make install ./configure make sudo make install ``` ```shell cp six_prover_executables /bin ``` -------------------------------- ### Frama-C Installation Commands for Mac OS X Source: https://frama-c.com/html/fc-discuss/2010-February/msg00031 This snippet demonstrates the essential commands required to install Frama-C on Mac OS X Snow Leopard. It includes commands for navigating directories, extracting tarballs, setting the PATH environment variable, and configuring the shell profile. These commands are crucial for making the Frama-C executable accessible from the terminal. ```bash cd / sudo tar jxvf /Users/Joao/Downloads/frama-c-Beryllium-20090902-why_2.23-OSX_intel.tar.bz2 export PATH=/usr/local/Frama-C_Be/bin:$PATH vi ~/.profile # and add line export PATH=/usr/local/Frama-C_Be/bin:$PATH ``` -------------------------------- ### Compile and Install Frama-C and Plugins (Shell) Source: https://frama-c.com/html/fc-discuss/2012-July/msg00024 This section details the process of compiling and installing Frama-C, its WP plugin, and the Jessie plugin via the Why3 toolchain. It involves navigating to source directories, running configure, make, and make install commands in a specific order to manage dependencies between Frama-C, Why3, and its plugins. ```shell # Compile and install Why3 first cd why3-0.71/ ./configure make sudo make install # Compile and install Frama-C cd frama-c-Nitrogen-20111001/ ./configure make sudo make install # Compile and install Jessie plugin via Why2.30 (requires Why3 and Frama-C) cd why-2.30/ ./configure make sudo make install # Upgrade WP plugin (optional, can be done at the end) cd wp-0.5-Nitrogen-20111001 autoconf ./configure make depend make sudo make install ``` -------------------------------- ### ACSL Example for Variadic Function Declaration Source: https://frama-c.com/html/fc-discuss/2010-April/msg00037 Provides an example of an ACSL (ANSI/ISO C Specification Language) contract for a variadic function like printf. This workaround allows for specifying contracts for functions with a variable number of arguments, which are not directly supported by the standard ACSL. ```c /*@ requires \valid(format); @ assigns \nothing; @*/ int printf(const char *format); ``` -------------------------------- ### C multi-line annotation example using one-line comments Source: https://frama-c.com/html/fc-discuss/2010-May/msg00033 This snippet demonstrates the use of one-line comments starting with '//@' to define multi-line annotations in C code, as discussed in the Frama-C mailing list. The example shows a predicate definition for an even integer. ```c //@ predicate even (integer x) = //@ x % 2 == 0; ``` -------------------------------- ### Example C Code with Function Pointer Call Source: https://frama-c.com/html/fc-discuss/2013-December/msg00027 This C code snippet defines a function pointer type and demonstrates its usage in a function call within `main`. This is the example code that the user intends to transform by replacing the function pointer call with a regular function call using a visitor. ```c /* --------------pfunc.c--------------------- */ typedef int p_func (int *, int); int main (p_func* func, int *arg1, int *arg2) { int result; result = (*func)(arg1, arg2); return result; } /*-------------end----------------*/ ``` -------------------------------- ### Frama-C ptests Configuration Example Source: https://frama-c.com/html/fc-discuss/2011-October/msg00005 This snippet demonstrates a Frama-C run configuration for 'ptests'. It shows how to use the `EXECNOW LOG` command to specify a log file and execute a command. The example highlights potential issues with relative paths for log files and the desired behavior for launching tests from different directory levels. It also poses a question about postprocessing options. ```text /* run.config CMD: frama-c OPT: -hello EXECNOW: LOG log.txt echo toto>result/log.txt */ This conf works fine if I launch ptest.byte directly in the unit-test dir : ptests.byte hello.c but if I launch it in the parent dir, the ptests fails : $ ptests.byte test1/hello.c No test path found And in the upper/upper dir, the cmd is incorrect due to path of generated log.txt $ ptests.byte tests/test1/hello.c % Dispatch finished, waiting for workers to complete /bin/sh: cannot create result/log.txt: Directory nonexistent Custom command failed: echo titi>result/log.txt % Comparisons finished, waiting for diffs to complete % Diffs finished. Summary: Run = 1 Ok = 0 of 1 stephane at vmu3cat03:~/IVERILOG/ESMERALDA/SVN/ESMERALDA/trunk/DEV/hello_world$ in fact I'd like to lauch the test at the different levels 2?) using postprocessing tool Is it possible to postprocess outputs of the frama-c run with an extra program ? I've seen EXECNOW, but it is a preprocess. Perhaps FILER option ? ``` -------------------------------- ### Frama-C Command Usage Example Source: https://frama-c.com/html/fc-discuss/2011-June/msg00025 Demonstrates the correct way to invoke Frama-C with specific options, addressing a user's confusion about command execution. Highlights the importance of including necessary options like '-jessie' to enable specific features. ```text On Sat, Jun 18, 2011 at 6:39 PM, Christofi Maria wrote: > Actually, when I am typing frama-c -jessie-why-opt="-fast-wp" test.c (if we suppose that the file was test.c), it is running gcc and that's all. > > So in my window, it appears preprocessing with "gcc -C -E -I test.c" and it finishes there. Is that normal? Am I doing something wrong? Ahem, you are doing two things wrong. One is replying to the mailing-list digest by quoting the entire digest and without changing the title. The other is forgetting the "-jessie" option. "-jessie-why-opt=?" only configures Jessie, but does not launch it. Pascal ``` -------------------------------- ### Frama-C WP Plugin Stuck Bug Report Example Source: https://frama-c.com/html/fc-discuss/2013-January/msg00013 This code snippet represents a C logic function 'pow' and a lemma 'pow_0' provided in a bug report to the Frama-C mailing list. The user experienced the 'frama-c -wp' plugin getting stuck when using the 'Typed' model. This example serves as a reproducible case for the bug. ```c /*@ logic integer pow(integer x, integer y) = y == 0 ? 1 : (x * pow(x, y - 1)); lemma pow_0: \forall integer x; pow(x, 0) == 1; */ ``` -------------------------------- ### Configure Script Output - System Checks Source: https://frama-c.com/html/fc-discuss/2017-August/msg00033 This output shows the results of the './configure' script execution, detailing checks for OCaml and its components, Frama-C, and Why3. It highlights detected versions and identifies missing tools like 'coqc' and 'pvs'. ```bash checking for ocamlc... ocamlc ocaml version is 4.03.0 ocaml library path is /Users/david/.opam/4.03.0/lib/ocaml checking for ocamlfind... yes checking OS dependent settings... Unix checking for ocamlopt... ocamlopt checking ocamlopt version... ok checking for ocamlc.opt... ocamlc.opt checking ocamlc.opt version... ok checking for ocamlopt.opt... ocamlopt.opt checking ocamlc.opt version... ok checking for ocamldep... ocamldep checking for ocamldep.opt... ocamldep.opt checking for ocamllex... ocamllex checking for ocamllex.opt... ocamllex.opt checking for ocamlyacc... ocamlyacc checking for ocamldoc... ocamldoc checking for ocamldoc.opt... ocamldoc.opt ocamlfind found ocamlgraph in /Users/david/.opam/4.03.0/lib/ocamlgraph checking for ocamlweb... true checking for frama-c... /Users/david/.opam/4.03.0/bin/frama-c checking Frama-c version... Silicon-20161101 checking for why3... /Users/david/.opam/4.03.0/bin/why3 checking Why3 version... configure: WARNING: unknown version , hope this works checking for coqc... no configure: WARNING: Cannot find coqc. checking for pvs... no configure: WARNING: Cannot find PVS. config.status: creating Makefile ``` -------------------------------- ### Frama-C Value Analysis Example for -slevel Option Source: https://frama-c.com/html/fc-discuss/2014-June/msg00030 This C code snippet is used to illustrate the impact of the -slevel option on Frama-C's Value analysis. It demonstrates how increasing -slevel changes the precision of the analysis results for variable 'x' by considering more execution paths. The code requires Frama-C to be installed for analysis. ```c /* Test this program with: frama-c -val -slevel 1 slevel-example.c and frama-c -val -slevel 2 slevel-example.c And look at the value of "x". With -slevel 1 we have "x ??? {2; 3; 4}" and with -slevel 2 with have "x ??? {2; 4}". Why? Because -slevel increases the number of different considered path for the analysis. In our program: -slevel | c | a | g(c,a) | x ------------------------------------------------------------------------------ 1 | c ??? {0; 1} | a ??? {2; 3} | g(c,a) ??? {(0,2); (1,2); | x ??? {2; 3; 4} | | | (0;3); (1,3)} | ------------------------------------------------------------------------------ 2 | | | | |-path 1 | c ??? {0} | a ??? {2} | g(c,a) ??? {(0,2)} | x ??? {2} -path 2 | c ??? {1} | a ??? {3} | g(c,a) ??? {(1,3)} | x ??? {4} | | | | aggregated| c ??? {0; 1} | a ??? {2; 3} | | x ??? {2; 4} result | I hope result of Frama-C analysis is clearer now. David Mentr??, 19th of June, 2014. */ extern int entropy_source; /*@ assigns \result \from entropy_source; assigns entropy_source \from entropy_source; ensures \result == 0 || \result == 1; */ int f(void); // f() returns indeterministically 0 or 1 int g(int x, int y) { return x + y; } void main(void) { int c; int a = 2; int x; c = f(); if (c) { a = 3; } x = g(c, a); } ``` -------------------------------- ### Frama-C Installation Problem and Environment Variable Setup Source: https://frama-c.com/html/fc-discuss/2009-January/msg00002 A user reports an installation problem with Frama-C on Windows, specifically with setting the FRAMAC_SHARE environment variable. The issue involves incorrect path concatenation leading to a 'cannot find prelude file' error during the Jessie analysis subprocess. The user demonstrates attempts with both Windows-style and forward-slash paths for the environment variable. ```shell FRAMAC_SHARE=C:\cygwin\usr\local\Frama-C FRAMAC_SHARE=C:/cygwin/usr/local/Frama-C frama-c -jessie-analysis -jessie-gui a.c Parsing [preprocessing] running gcc -C -E -I. -include /usr/local/share/frama-c\jessie\jessie_prolog.h -dD a.c Cleaning unused parts Symbolic link Starting semantical analysis Starting Jessie translation Producing Jessie files in subdir a.jessie File a.jessie/a.jc written. File a.jessie/a.cloc written. Calling Jessie tool in subdir a.jessie Generating Why function max Calling VCs generator. gwhy-bin [...] why/a.why cannot find prelude file /usr/local/share/frama-c/why\why\prelude.why make: *** [a.stat] Error 1 Jessie subprocess failed: make -f a.makefile gui ```