Frama-C

https://frama-c.com/html/
Admin
Frama-C is a framework for analyzing C programs with support for formal verification, static...
Tokens:1,267,293
Snippets:8,856
Trust Score:9.6
Update:10 months ago
Show doc for...
Tokens:
Raw
### 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 <sstream>
 #include <vector>
 #include <map>
+#include <string.h>
 #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 <malloc.h>
+
 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 <fstream>

 #include "debug.h"
-    
+#include <cstdlib>
 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 <limits.h>
 #include <sstream>
 #include <gmp.h>

=== 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<i ==> 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<i.
```

--------------------------------

### Frama-C GUI Analysis Example

Source: https://frama-c.com/html/fc-discuss/2014-September/msg00002

Shows the command to launch the Frama-C GUI directly with a source file, enabling value analysis (-val) and displaying warnings in the Messages panel. This serves as a baseline for comparison with the -save/-load workflow.

```bash
frama-c-gui -val warn.c
```

--------------------------------

### Ubuntu Z3 Installation and Frama-c Integration

Source: https://frama-c.com/html/fc-discuss/2009-May/msg00055

This snippet provides a step-by-step guide for installing the Z3 prover on Ubuntu using Wine and integrating it with Frama-c. It includes shell commands for setting up the environment and a script to link the Z3 executable.

```shell
1) download z3-1.3.6.msi Latest version: Z3
1.3<http://research.microsoft.com/research/downloads/details/0a7db466-c2d7-4c51-8246-07e25900c7e7/details.aspx>
. 
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
<Maria.Christofi at gemalto.com> 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
```
Tokens:
Raw