SEAL is a static analyzer for C programs built in OCaml. The tool is built to detect memory safety bugs and to verify the correctness of programs that work with linked lists. The analysis method is based on dataflow analysis with separation logic as the abstract domain.

This installation guide was tested on Fedora 41 and Ubuntu 24.04, but it should work on any recent Linux distribution.

• Install OCaml using this guide.

• Install the necessary dependencies:

  opam install . --deps-only

• Install the Astral solver outside of this repository:

  git clone https://github.com/TDacik/Astral.git
  cd Astral
  git checkout dev-stable
  opam install .

• Build and install SEAL. Inside this repository, run:

  dune build
  dune install

To run the analysis of a single program in the terminal, use:

frama-c -seal <filename.c>

To run with the recommended settings in Ivette (Frama-C GUI), use:

make run <filename.c>

Note: when running Ivette for the first time, you need to install its dependencies according to instructions printed to the terminal

To run with the recommended settings without constant propagation and loop unrolling, use:

make run-direct <filename.c>

To run the full benchmark suite, you must first clone the repository with SV-COMP benchmarks into ../sv-benchmarks relative to this repository:

git clone https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks.git ../sv-benchmarks --depth 1 --branch svcomp25

Then, you can run the benchmarks and display the results:

make benchmark
make results

Note: for running benchmarks, you need to first install Benchexec using this guide.

Results of the analysis displayed in Ivette (Frama-C GUI frontend):

• -seal - Enable the analysis
• -seal-astral-debug - Print debug info about queries to Astral
• -seal-astral-encoding <Bitvectors | Sets> - Which location encoding should Astral use, default: Bitvectors
• -seal-backend-solver <Auto | Bitwuzla | CVC5 | Z3> - Which solver should be used by Astral, default: Auto
• -seal-svcomp-mode - Enables features needed to run SV-COMP benchmarks
• -seal-catch-exceptions - Catch exceptions in main function (disable this for benchmarks) (set by default, opposite option is -seal-no-catch-exceptions)
• -seal-dump-queries - Dump Astral queries to the astral_queries directory.
• -seal-edge-abstraction - Do abstraction on every edge between statements (default: abstraction is done on loop return)
• -seal-edge-deduplication - Deduplicate states on every edge between statements
• -seal-max-loop-cycles <N> - If set, the analysis will traverse loops only N times
• -seal-print-sort - Print sort of variables along with their names
• -seal-simple-join - Compute join of states using entailment on single formulae (default: entailments of disjunctions are computed)

├── bench -- files for running Benchexec benchmarks
│   ├── seal -- Benchexec tool definition for SEAL
│   │   ├── __init__.py
│   │   └── seal.py
│   ├── seal-results.xml -- Description for rendering HTML results
│   ├── seal.xml -- Definition of SV-COMP and custom benchmarks
│   └── setup.py
├── bp -- Typst source files and assets for the thesis
│   ├── ...
│   ├── template.typ
│   └── main.typ -- Text of the thesis
├── dune-project -- OCamp project declaration
├── excel_at_fit -- Poster and abstract from Excel@FIT 2025
│   ├── abstract.pdf
│   └── poster.pdf
├── Makefile -- makefile with useful shortcut commands
├── README.md
├── src -- Source code of the analyzer
│   ├── ...
│   ├── analysis.ml
│   └── formula.ml
├── test_programs -- Collection of custom tests for the analyzer
│   ├── ...
│   ├── nls_memory_leak.c -- Test program
│   └── nls_memory_leak.yml -- benchmark declaration for Benchexec
└── thesis.pdf -- Final PDF of the thesis

• src/main.ml - entrypoint of the analyzer, runs all phases of the analysis in order and handles exceptions that signify found bugs, uses analysis.ml and preprocessing.ml
• src/analysis.ml - implements the dataflow analysis interface required by Frama-C, uses transfer.ml, simplification.ml, and abstraction.ml
• src/transfer.ml - implements the transfer function for dataflow analysis, uses func_call.ml
• src/func_call.ml - implements interprocedural analysis (transfer function for function calls)
• src/simplification.ml - implements most of the formula simplifications
• src/abstraction.ml - implements the abstraction of spatial atoms into list predicates
• src/astral_query.ml - wrapper for the Astral solver's API, implements caching of queries
• src/formula.ml - module that implements the type representing SL formulae in the analysis, and a set of functions for their manipulation
• src/preprocessing/preprocessing.ml - entrypoint of all preprocessing, implements multiple simple preprocessing passes
• src/preprocessing/types.ml - implements the analysis of C types that determines, which type of linked list they represent
• src/preprocessing/block_builder.ml - implements splitting expressions into a series of basic assignments
• src/preprocessing/condition_split.ml - implements preprocessing of conditional statements
• src/preprocessing/stmt_split.ml - implements preprocessing of assignments and function calls
• src/preprocessing/instruction_type.ml - implements the type representing the basic instructions, for which the transfer function is implemented
• src/preprocessing/constants.ml - contains common constants used by the preprocessing passes
• src/common.ml - common code used by other modules
• src/config.ml - definitions of command-line parameters
• src/printing.ml - definines categories of debug output
• src/ivette.ml - definitions of data exposed to Ivette (Frama-C GUI)
• src/testing.ml - utility functions for unit tests in other modules, unit tests for the formula.ml module