forked from seahorn/seahorn
-
Notifications
You must be signed in to change notification settings - Fork 0
Documents
Yusen Su edited this page May 24, 2023
·
6 revisions
- Installing SeaHorn: Instructions for SeaHorn installation.
- SeaHorn tools: Overview of the main tools provided by SeaHorn.
- SeaHorn options: Overview of the main command-line options used for verification.
- Writing unit proofs: Instructions for writing verification tasks.
- SeaBMC: Overview of how verification conditions generated by SeaHorn.
To get the most recently version of SeaHorn, we provide a Docker container which builds SeaHorn nightly.
Using the following command to pull the nightly built container:
$ docker pull seahorn/seahorn-llvm14:nightly
The dockerfile to build a container locally is provided in the docker folder. The instructions are provided in README.md.
- Sets the environment for verification (pre-condition)
- Calls function under verification
- Validates the result (post-condition)
To provide the context of specific operations or calculations for verification, SeaHorn offers a collection of built-in functions declared in include/seahorn/seahorn.h including:
-
assume(bool)
: set a condition to be assumed as "true" by the verifier.
Spatial memory safety is xxx.[TODO]
-
bool sea_is_dereferenceable(const void *ptr, intptr_t offset)
: