### Start Frama-C Server with ZeroMQ

Source: https://github.com/pub/frama-c/blob/master/src/plugins/server/doc/server_zmq.md

Example command to start a Frama-C server using the ZeroMQ protocol for inter-process communication.

```shell
$ frama-c [options...] -then -server-zmq ipc:///tmp/my-server.io
```

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

### Install Frama-C

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Install Frama-C and its plugins using the make install command. May require superuser privileges depending on the installation directory.

```shell
make install
```

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

### Test Frama-C Installation with Example C Files

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Run Frama-C analysis on downloaded test files to verify the installation. Supports both frama-c and ivette executables.

```shell
frama-c -eva test/CruiseControl*.c
# or (if ivette is available)
ivette -eva test/CruiseControl*.c
```

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

### Install Frama-C Development Branch

Source: https://github.com/pub/frama-c/blob/master/README.md

Pin the development version of Frama-C to install the latest nightly build. If installation fails due to missing dependencies, use the standard installation commands to get them first.

```bash
opam pin add frama-c --dev-repo
```

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

### Install Frama-C Loop Analysis Plugin

Source: https://github.com/pub/frama-c/blob/master/src/plugins/loop_analysis/README.org

Manual installation of the Frama-C loop analysis plugin. Ensure Frama-C is installed before proceeding.

```bash
make
make install
```

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

### Install Frama-C with opam < 2.1

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

For opam versions older than 2.1, first install the 'depext' utility, then use it to install Frama-C's dependencies before installing Frama-C itself.

```shell
opam install depext
opam depext frama-c
opam install frama-c
```

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

### Run Test Receiver Server

Source: https://github.com/pub/frama-c/blob/master/src/plugins/e-acsl/examples/ensuresec/README.md

Start the Flask test server to listen for and print JSON alerts. Ensure Flask is installed.

```bash
FLASK_APP=receiver.py FLASK_ENV=development flask run
```

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

### Build and Install Ivette

Source: https://github.com/pub/frama-c/blob/master/ivette/README.md

Builds a distributable version of Ivette and then installs it on the system. Ensure Frama-C is configured before running.

```sh
make -C ivette dist
[sudo] make -C ivette install
```

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

### Install Frama-C with Dune

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Install Frama-C using the dune install command. This is often used in conjunction with make install.

```shell
dune install
```

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

### Example .env File for Wrapper Script

Source: https://github.com/pub/frama-c/blob/master/src/plugins/e-acsl/examples/ensuresec/README.md

An example configuration file specifying environment variables required by the wrapper.py script.

```dotenv
export ENSURESEC_EE_ID="your_ecosystem_id"
export ENSURESEC_EE_TOOL_ID="your_tool_id"
export ENSURESEC_OUTPUT_FILE="./ensuresec_ee.json"
```

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

### Get Plug-in Help

Source: https://github.com/pub/frama-c/blob/master/README.md

Use this command format to get help specific to a Frama-C plug-in, including its options.

```bash
-<plugin>-help
```

```bash
-<plugin>-h
```

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

### Initialize Opam and Install Dependencies on WSL

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Initialize opam without sandboxing and set up the environment. Installs the 'depext' package for dependency management.

```shell
opam init --disable-sandboxing --shell-setup
eval $(opam env)
opam install -y depext
```

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

### Install Executables

Source: https://github.com/pub/frama-c/blob/master/tests/mopsa/polarssl-cmake.t/programs/pkey/CMakeLists.txt

Installs the specified executables to the 'bin' directory with defined permissions. This ensures the programs are accessible after installation.

```cmake
install(TARGETS dh_client dh_genprime dh_server key_app mpi_demo rsa_genkey rsa_sign rsa_verify rsa_encrypt rsa_decrypt
        DESTINATION "bin"
        PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
```

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

### Run Ensuresec Example Wrapped with Alert Pushing

Source: https://github.com/pub/frama-c/blob/master/src/plugins/e-acsl/examples/ensuresec/README.md

Execute the Ensuresec example and push its alerts to a running test server. The test server must be launched beforehand.

```bash
make run_wrapped
```

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

### Install SSL Executables

Source: https://github.com/pub/frama-c/blob/master/tests/mopsa/polarssl-cmake.t/programs/ssl/CMakeLists.txt

Installs the compiled SSL client and server executables to the 'bin' directory with appropriate permissions.

```cmake
install(TARGETS ssl_client1 ssl_client2 ssl_server ssl_fork_server ssl_mail_client
        DESTINATION "bin"
        PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
```

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

### Launch Ensuresec Alert Receiver

Source: https://github.com/pub/frama-c/blob/master/src/plugins/e-acsl/examples/ensuresec/README.md

Start the test server to receive alerts pushed from the Ensuresec example. This should be run in a secondary terminal.

```bash
make launch_receiver
```

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

### Run Ensuresec Example with JSON Output

Source: https://github.com/pub/frama-c/blob/master/src/plugins/e-acsl/examples/ensuresec/README.md

Execute the compiled Ensuresec e-commerce example. Alerts are saved to a JSON file.

```bash
make run
```

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

### Run Aoraï and WP for Loop Example in One Go

Source: https://github.com/pub/frama-c/blob/master/doc/aorai/example/README.md

Execute Aoraï instrumentation and WP verification for the loop example within a single Frama-C execution.

```sh
frama-c example_loop.c -aorai-automata example_loop.ya -then-last -wp
```

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

### Install Executable Targets

Source: https://github.com/pub/frama-c/blob/master/tests/mopsa/polarssl-cmake.t/programs/test/CMakeLists.txt

This command installs the specified executable targets to the 'bin' directory with execute permissions for owner, group, and world. This ensures the built programs are accessible after installation.

```cmake
install(TARGETS selftest benchmark ssl_test ssl_cert_test
        DESTINATION "bin"
        PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
```

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

### Install Frama-C Dependencies and Frama-C on WSL

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Installs required lablgtk3 packages and Frama-C itself using opam, ensuring all dependencies are met.

```shell
opam depext --install -y lablgtk3 lablgtk3-sourceview3
opam depext --install -y frama-c
```

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

### Compile and Install Specific Frama-C Tools Manually

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Build and install a specific Frama-C tool by navigating to its directory within the tools folder. This is an alternative to the global developer mode installation.

```shell
make -C tools/<the-tool>
make -C tools/<the-tool> install
```

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

### Building, Installing, and Using Frama-C Plugin

Source: https://context7.com/pub/frama-c/llms.txt

Commands to build and install the OCaml plugin using Dune, and then use it with Frama-C, including verifying its registration.

```bash
# Build and install
dune build
dune install

# Use the plugin
frama-c -checker file.c
frama-c -checker -checker-depth 5 file.c

# Verify it's registered
frama-c -plugins | grep checker

```

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

### Install opam on macOS

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Use Homebrew to install the opam package manager, which is recommended for Frama-C installation on macOS.

```shell
brew install opam
```

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

### Install Executables (CMake)

Source: https://github.com/pub/frama-c/blob/master/tests/mopsa/polarssl-cmake.t/programs/hash/CMakeLists.txt

Installs the specified executable targets to the 'bin' directory with defined permissions. This ensures the programs are accessible after installation.

```cmake
install(TARGETS hello md5sum sha1sum sha2sum generic_sum
        DESTINATION "bin"
        PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
```

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

### Install Frama-C on Fedora

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Install Frama-C using the dnf package manager on Fedora systems.

```shell
dnf install frama-c
```

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

### Install Node.js and Yarn on macOS

Source: https://github.com/pub/frama-c/blob/master/ivette/README.md

Installs Yarn and nvm using Homebrew, then installs and uses Node.js version 24.x on macOS.

```sh
brew install yarn
brew install nvm # follow instructions
nvm install 24
nvm use 24
```

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

### Install Frama-C on Debian/Ubuntu

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Install Frama-C using the apt-get package manager on Debian-based systems.

```shell
apt-get install frama-c
```

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

### Install Frama-C on Arch Linux

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Install Frama-C using the pikaur AUR helper on Arch Linux.

```shell
pikaur -S frama-c
```

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

### Get Frama-C Kernel Help

Source: https://github.com/pub/frama-c/blob/master/README.md

Retrieve a list of options that control the behavior of Frama-C's core kernel.

```bash
frama-c -kernel-help
```

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

### Install PolarSSL Target

Source: https://github.com/pub/frama-c/blob/master/tests/mopsa/polarssl-cmake.t/library/CMakeLists.txt

Installs the built PolarSSL library to the specified installation directory with read, write, and execute permissions for owner, group, and others.

```cmake
install(TARGETS polarssl
        DESTINATION ${LIB_INSTALL_DIR}
        PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
```

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

### Install Frama-C Plugins with Dune

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Use this command to build and install Frama-C plugins released independently. Ensure you are in the correct directory.

```shell
dune build @install && dune install
```

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

### Install Frama-C via opam

Source: https://github.com/pub/frama-c/blob/master/README.md

Use this command to install Frama-C using the OCaml package manager. For older opam versions, install depext first to handle external dependencies.

```bash
opam install frama-c
```

```bash
opam install depext # handles external (non-OCaml) dependencies
opam depext frama-c --install
```

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

### Install Custom Frama-C Version with Opam

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Use this command to install a custom Frama-C version from a local directory using opam. Ensure Frama-C's dependencies are installed first.

```shell
opam remove --force frama-c
opam install depext # only for opam < 2.1.0
opam depext frama-c # only for opam < 2.1.0
opam install --deps-only frama-c [--with-test]
opam pin add --kind=path frama-c <dir>
```

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

### Install Executables in CMake

Source: https://github.com/pub/frama-c/blob/master/tests/mopsa/polarssl-cmake.t/programs/x509/CMakeLists.txt

This snippet defines installation rules for the 'cert_app' and 'crl_app' executables. They are installed into the 'bin' directory with specific file permissions for the owner, group, and others.

```cmake
install(TARGETS cert_app crl_app
        DESTINATION "bin"
        PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
```

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

### Compile and Install Frama-C on Linux

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Compile Frama-C in release mode and install it. This command assumes dependencies are met.

```shell
make RELEASE=yes && make install
```

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

### Frama-C Output and Help

Source: https://context7.com/pub/frama-c/llms.txt

Commands to display normalized C output and list available plugins or get help for specific plugins.

```bash
# Display normalized C output
frama-c file.c -print -ocode normalized.c
```

```bash
# List all loaded plugins
frama-c -plugins
```

```bash
# Get help for a specific plugin
frama-c -eva-help
frama-c -wp-help
```

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

### Install Frama-C with opam >= 2.1

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Use this command to install Frama-C and its dependencies if you have opam version 2.1 or newer. Opam handles system package dependencies automatically.

```shell
opam install frama-c
```

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

### Build Frama-C in Development Mode

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Build Frama-C in development mode using make, which is a shortcut for 'dune build @install'.

```shell
make
```

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

### Download Frama-C Test Files

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Download necessary C source and header files for testing Frama-C installation using wget.

```shell
export PREFIX_URL="https://git.frama-c.com/pub/frama-c/raw/master/tests/value"
wget -P test ${PREFIX_URL}/CruiseControl.c
wget -P test ${PREFIX_URL}/CruiseControl_const.c
wget -P test ${PREFIX_URL}/CruiseControl.h
wget -P test ${PREFIX_URL}/CruiseControl_extern.h
wget -P test ${PREFIX_URL}/scade_types.h
wget -P test ${PREFIX_URL}/config_types.h
wget -P test ${PREFIX_URL}/definitions.h
```

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

### Install Frama-C Dependencies with Opam

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Use opam to install Frama-C dependencies. Ensure opam version compatibility for specific commands.

```shell
opam install depext # only for opam < 2.1.0
opam depext frama-c # only for opam < 2.1.0
opam install --deps-only frama-c
```

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

### Install PolarSSL Binaries

Source: https://github.com/pub/frama-c/blob/master/tests/mopsa/polarssl-cmake.t/programs/aes/CMakeLists.txt

Installs the built 'aescrypt2' and 'crypt_and_hash' executables into the 'bin' directory with standard read, write, and execute permissions for the owner, and read and execute permissions for the group and others.

```cmake
install(TARGETS aescrypt2 crypt_and_hash
        DESTINATION "bin"
        PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
```

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

### Install Node.js and Yarn on Linux

Source: https://github.com/pub/frama-c/blob/master/ivette/README.md

Installs Node Version Manager (nvm), Node.js version 24.x, and Yarn globally on Linux systems.

```sh
curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.40.3/install.sh | bash
nvm install 24
nvm use 24
npm install --global yarn
```

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

### Install Frama-C Dependencies using Opam Pin

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Fetch and build all Frama-C dependencies using opam after pinning the development version.

```shell
opam install --deps-only .
```

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

### Manual Frama-C Installation in Developer Mode

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Compile and install Frama-C manually in developer mode using the FRAMAC_DEVELOPER environment variable. This method is useful for plugin developers.

```shell
FRAMAC_DEVELOPER=yes make
FRAMAC_DEVELOPER=yes make install
```

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

### Run Ensuresec Example Outputting All Assertions

Source: https://github.com/pub/frama-c/blob/master/src/plugins/e-acsl/examples/ensuresec/README.md

Execute the compiled program from 'compile_print_all', which outputs all assertions.

```bash
make run_print_all
```

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

### Basic Makefile for Dome Application

Source: https://github.com/pub/frama-c/blob/master/ivette/src/dome/README.md

This makefile includes the Dome template and sets up the default development target. Ensure Yarn and Node are installed.

```makefile
include dome/template/makefile
all: dome-dev
```

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

### Pin Frama-C Additional Tools with Opam

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Install frama-c-lint and frama-c-hdrck by pinning their respective tool directories using Opam. This is an alternative to manual compilation.

```shell
opam pin tools/lint
```

```shell
opam pin tools/hdrck
```

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

### List Frama-C Plug-ins

Source: https://github.com/pub/frama-c/blob/master/README.md

Execute this command to display a list of all available plug-ins for Frama-C.

```bash
frama-c -plugins
```

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

### Basic Frama-C Command-Line Usage

Source: https://context7.com/pub/frama-c/llms.txt

Demonstrates basic command-line invocations for parsing and analyzing C files with Frama-C. Use `-eva` to run the Eva plugin.

```bash
# Parse a file and run Eva value analysis
frama-c -eva file.c
```

```bash
# Run Eva on multiple files with a custom entry point
frama-c -main my_entry -eva src/main.c src/util.c
```

```bash
# Preprocess with custom defines and include paths, then analyze
frama-c -cpp-extra-args="-DDEBUG -I./include" -eva file.c
```

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

### Install Random Generator Executables

Source: https://github.com/pub/frama-c/blob/master/tests/mopsa/polarssl-cmake.t/programs/random/CMakeLists.txt

Installs the 'gen_random_havege', 'gen_random_ctr_drbg', and 'gen_entropy' executables to the 'bin' directory with specific file permissions. This ensures the programs are accessible after installation.

```cmake
install(TARGETS gen_random_havege gen_random_ctr_drbg gen_entropy
        DESTINATION "bin"
        PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
```

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

### Display frama-c-lint Help Information

Source: https://github.com/pub/frama-c/blob/master/tools/lint/README.md

Use the -help option to display all available command-line options for the frama-c-lint tool. This includes information on configuration files, verbose mode, and update functionalities.

```bash
> frama-c-lint -help
Usage: git ls-files -z | git check-attr --stdin -z -a | _build/install/default/bin/frama-c-lint [options]

Checks or updates files in relation to lint constraints specified by these git attributes:
  check-eoleof, check-syntax, check-utf8 and check-indent.

Options:
  --version        Prints tool version
  -c <json-config-file> Reads the JSON configuration file (allows to overload the default configuration)
  -e               Prints default JSON configuration
  -s               Considers warnings as errors for the exit value
  -u               Update ill-formed files (does not handle UTF8 update)
  -v               Verbose mode
  -help            Display this list of options
  --help           Display this list of options
```

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

### Emacs Package Installation for TypeScript Development

Source: https://github.com/pub/frama-c/blob/master/ivette/CONTRIBUTING.md

Commands to install necessary Emacs packages for TypeScript and web development. Ensure your package index is up-to-date before installing.

```emacs-lisp
M-x package-refresh-contents ;; updates your index
M-x package-install web-mode
M-x package-install typescript-mode
M-x package-install tide
```

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

### Install PolarSSL Headers with CMake

Source: https://github.com/pub/frama-c/blob/master/tests/mopsa/polarssl-cmake.t/include/CMakeLists.txt

This snippet conditionally installs PolarSSL header files. It uses file(GLOB) to find headers and install() to copy them to the specified destination with read/write permissions.

```cmake
option(INSTALL_POLARSSL_HEADERS "Install PolarSSL headers." ON)

if(INSTALL_POLARSSL_HEADERS)

file(GLOB headers "polarssl/*.h")

install(FILES ${headers}
        DESTINATION include/polarssl
        PERMISSIONS OWNER_READ OWNER_WRITE GROUP_READ WORLD_READ)

endif(INSTALL_POLARSSL_HEADERS)
```

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

### Configure Message Keys with Command Line Options

Source: https://github.com/pub/frama-c/blob/master/Changelog_detailed.md

Demonstrates how to use command-line options to manage message keys for Frama-C plug-ins and kernel. Options like -plugin-msg-key, -plugin-msg-unset, and -plugin-msg-set allow fine-grained control over message display.

```bash
-plugin-msg-key a -plugin-msg-unset a:b -plugin-msg-set a:b:c
```

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

### Strategy Syntax Example

Source: https://github.com/pub/frama-c/blob/master/ivette/src/frama-c/plugins/wp/doc.md

Illustrates the expected syntax for defining a strategy in the Strategy Debugger. The 'name' field is optional, and strategies can be composed of multiple alternatives, tactics, and existing strategies.

```frama-c
name: (optional)
  	tactic(
    "Wp.range",
    	pattern(i <= 31),
    	param("inf", 0),
    	param("sup", 31)),
  	tactic(
    "Wp.split",
    	pattern(A && B)),
  existing_strategy
```

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

### Frama-C Multi-Step Workflows

Source: https://context7.com/pub/frama-c/llms.txt

Shows how to save and load Frama-C analysis states, and chain plugins sequentially. Use `-save` to store results and `-load` to resume.

```bash
# Save parse result, then reload for analysis (two-step workflow)
frama-c *.c -cpp-extra-args="-I./include" -save parsed.sav
frama-c -load parsed.sav -eva -eva-precision 5
```

```bash
# Run Eva then Slicing in sequence
frama-c file.c -eva -then -slice-return main -then-last -ocode sliced.c
```

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

### Frama-C Project Save/Load Workflow

Source: https://context7.com/pub/frama-c/llms.txt

Demonstrates saving an initial parse to a project file and then loading it for subsequent analyses like Eva and WP, and for slicing.

```bash
# Step 1: Parse once and save
frama-c -cpp-extra-args="-I./include -DPLATFORM_X64" \
        src/*.c -save parsed.sav

# Step 2a: Run Eva from saved parse
frama-c -load parsed.sav -eva -eva-precision 5 -save eva.sav

# Step 2b: Run WP from saved parse (independent of Eva)
frama-c -load parsed.sav -wp -wp-rte -save wp.sav

# Step 3: Load Eva results for slicing
frama-c -load eva.sav \
        -slice-return main \
        -then-last -ocode sliced.c

```

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

### Plugin Resources Configuration

Source: https://github.com/pub/frama-c/blob/master/ivette/src/sandbox/sandbox.md

Example of how to configure the 'pkg.json' file to include resources from a plugin, specifically for loading images. This ensures that plugin assets are loaded only when the plugin is active.

```json
{
  "name": "Frama-C/Eva",
  "resources": ["./images/"]
}
```

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

### Run Frama-C Basic Tests

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Execute basic tests for Frama-C using the make command.

```shell
make run-ptests
```

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

### Install Yarn on Arch Linux

Source: https://github.com/pub/frama-c/blob/master/ivette/README.md

Installs the Yarn package and its Node.js dependency using pacman on Arch Linux.

```sh
pacman -S yarn
```

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

### Initialize WP Cache

Source: https://github.com/pub/frama-c/blob/master/src/plugins/wp/tests/README.md

Initiates the WP-cache by cloning the repository if it's the first execution, or pulling the latest entries on subsequent runs. This command is necessary before executing WP tests in the 'qualif' configuration.

```bash
$ ./bin/test.sh -p
```

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

### Install Opam Packages on WSL

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Commands to update the system and install necessary packages for opam on a Debian-based Linux distribution within WSL.

```shell
sudo apt update
sudo apt upgrade
sudo apt install make m4 gcc opam gnome-icon-theme
```

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

### ACSL Function Contract Example

Source: https://context7.com/pub/frama-c/llms.txt

An example of an ACSL function contract specifying preconditions, postconditions, and assigned memory regions for the `array_sum` function.

```c
/*@ 
  requires n >= 0;
  requires \valid_read(a + (0..n-1));
  assigns  \nothing;
  ensures  \result == sum(a, 0, n);
  ensures  \result >= 0 || n == 0;
*/
int array_sum(int *a, int n) {
```

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

### Run Frama-C GUI on WSL2 with Wayland Issue

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Prefix the Frama-C GUI command with GDK_BACKEND=x11 to work around Wayland compatibility issues on WSL2.

```shell
GDK_BACKEND=x11 frama-c-gui <options>
```

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

### Typed memcpy Specification Example

Source: https://github.com/pub/frama-c/blob/master/src/plugins/instantiate/README.md

Example of a typed specification for memcpy, specialized for integer pointers, which can be efficiently used by plugins like WP.

```c
/*@ requires valid_dest: \valid(dest + (0 .. len-1));
    requires valid_read_src: \valid_read(src + (0 .. len-1));
    requires separation: \separated(dest + (0 .. len-1), src + (0 .. len-1));
    ensures copied: ∀ ℤ j0; 0 ≤ j0 < len ⇒ *(dest + j0) ≡ *(src + j0);
    ensures result: \result ≡ dest;
    assigns *(dest + (0 .. len - 1)), \result;
    assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
    assigns \result \from dest;
 */
int *memcpy_int(int *dest, int const *src, size_t len);
```

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

### Run Frama-C Test Framework

Source: https://github.com/pub/frama-c/blob/master/CONTRIBUTING.md

Execute the Frama-C test suite locally by running `make default-tests` from the project's root directory.

```shell
make default-tests
```

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

### Build Crypt and Hash Example with PolarSSL

Source: https://github.com/pub/frama-c/blob/master/tests/mopsa/polarssl-cmake.t/programs/aes/CMakeLists.txt

Defines an executable for the 'crypt_and_hash' example and links it against the PolarSSL library. This is used to build a utility for cryptographic operations and hashing.

```cmake
add_executable(crypt_and_hash crypt_and_hash.c)
target_link_libraries(crypt_and_hash polarssl)
```

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

### Build AES Crypt Example with PolarSSL

Source: https://github.com/pub/frama-c/blob/master/tests/mopsa/polarssl-cmake.t/programs/aes/CMakeLists.txt

Defines an executable for the 'aescrypt2' example and links it against the PolarSSL library. This is used to build a standalone AES encryption utility.

```cmake
add_executable(aescrypt2 aescrypt2.c)
target_link_libraries(aescrypt2 polarssl)
```

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

### Build Frama-C in Release Mode

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Build Frama-C in release mode using make, which is a shortcut for 'dune build @install --release --promote-install-files=false'.

```shell
make RELEASE=yes
```

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

### Makefile Workflow for Frama-C Analysis

Source: https://context7.com/pub/frama-c/llms.txt

Set up a reproducible analysis workflow using `frama-c-script` and Makefile templates. This includes initial project setup, defining analysis targets, and running analyses with caching.

```bash
# Initial project setup
cd myproject
mkdir .frama-c
cp "$(frama-c -print-share-path)/analysis-scripts/template.mk" .frama-c/GNUmakefile
alias fcmake='make -C .frama-c'
```

```makefile
# .frama-c/GNUmakefile — customized template

# Architecture
MACHDEP = x86_64

# Preprocessing flags
CPPFLAGS = -I../include -DNDEBUG

# Frama-C global flags
FCFLAGS = -main app_main

# Eva flags
EVAFLAGS = -eva-precision 5 -eva-slevel 100

# Analysis targets
TARGETS = app.eva

# Source files for parsing target
app.parse: ../src/main.c ../src/util.c ../src/net.c

# Optional: per-target overrides
app.parse: CPPFLAGS += -DPLATFORM_LINUX

```

```bash
# Parse (result cached in .frama-c/app.parse/)
fcmake app.parse
```

```bash
# Run Eva analysis (cached)
fcmake app.eva
```

```bash
# Open results in Ivette GUI
fcmake app.eva.ivette
```

```bash
# Re-run only changed parts
touch ../src/main.c
fcmake app.eva   # automatically re-parses and re-analyzes
```

```bash
# Generate SARIF report for CI integration
fcmake app.parse
frama-c -load .frama-c/app.parse/framac.sav \
        -eva -mdr-gen sarif -mdr-out report.sarif
```

```bash
# Use JSON compilation database (from CMake/Bear)
cmake -DCMAKE_EXPORT_COMPILE_COMMANDS=1 .
frama-c-script list-files         # list files in database
frama-c -compilation-db compile_commands.json main.c
```

```bash
# Find a function across the codebase
frama-c-script find-fun my_function ./src
```

```bash
# Normalize paths in a compilation database
frama-c-script normalize-jcdb compile_commands.json
```

```bash
# Visualize analysis performance flamegraph
frama-c-script flamegraph .frama-c/app.eva/framac.sav flamegraph.svg
```

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

### Configure WSL 1 for Frama-C GUI

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Set environment variables in WSL 1 to enable the Frama-C GUI when an X server is running on Windows.

```shell
export LIBGL_ALWAYS_INDIRECT=1
export DISPLAY=:0
frama-c-gui
```

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

### Build Frama-C with Dune (Development)

Source: https://github.com/pub/frama-c/blob/master/INSTALL.md

Build Frama-C in development mode directly using the dune build command.

```shell
dune build @install
```

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

### Eva Plugin: Value Analysis Example

Source: https://context7.com/pub/frama-c/llms.txt

A C code example demonstrating a potential buffer overflow bug. The Eva plugin can detect this type of runtime error.

```c
// rte_example.c
#include <stdio.h>

int t[10];

void fill(int n) {
  int i;
  /*@ loop assigns i, t[0..n-1];
      loop invariant 0 <= i <= n;
      loop variant n - i;
  */
  for (i = 0; i <= n; i++)   // Bug: should be i < n
    t[i] = i;
}

int main(void) {
  fill(9);
  return 0;
}
```