Skip to content

Commit

Permalink
Documentation improviments
Browse files Browse the repository at this point in the history
  • Loading branch information
janislley committed Sep 16, 2023
1 parent 91cf164 commit 9608637
Showing 1 changed file with 19 additions and 5 deletions.
24 changes: 19 additions & 5 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,15 @@
## LSVerifier

LSVerifier is a command-line tool for formal verification of large ANSI-C projects in a single run. It leverages the [ESBMC](https://github.com/esbmc/esbmc) model checker as its core verification engine.
LSVerifier is a command-line tool for formal verification of large ANSI-C projects in a single run.

It leverages the [ESBMC](https://github.com/esbmc/esbmc) model checker as its core verification engine.

## Version

| Version | Improviments |
|---------|--------------|
| v0.3.0 | Support specific class of property verification; Prioritized functions verification, Disable invalid pointer verification. |
| v0.2.0 | Support for libraries dependencies; Recursive verification for large software. |

## Installation

Expand Down Expand Up @@ -32,7 +41,7 @@ $ pip3 install lsverifier
#### 1. Verify a project
```
$ cd <project-root>
$ lsverifier -r -f .
$ lsverifier -r -f
```

For projects with third-party library dependencies, use ```-l``` option to specify header paths:
Expand All @@ -46,6 +55,11 @@ See an example of ```dep.txt``` below:
```
/usr/include/glib-2.0/
/usr/lib/x86_64-linux-gnu/glib-2.0/include/extcap/
extcap/
plugins/epan/ethercat/
plugins/epan/falco_bridge/
plugins/epan/wimaxmacphy/
epan/crypt/
...
```

Expand All @@ -61,15 +75,15 @@ If you want to verify a project using a prioritization scheme, run:

```
$ cd <project-root>
$ lsverifier -r -fp .
$ lsverifier -r -fp
```

#### 4. Verify an entire project by providing the folder path as an argument

To set the folder path parameter, you should use ```-d```:

```
lsverifier -r -f -i dep.txt -d project-root/
lsverifier -r -f -l dep.txt -d project-root/
```

#### 5. LSVerifier help
Expand All @@ -86,7 +100,7 @@ Input Options
optional arguments:
-h, --help show this help message and exit
-l,--libraries LIBRARIES
Path to the file that describes the libraries dependencies
Path to the file that describes the libraries' dependencies
-p,--properties PROPERTIES
Properties to be verified (comma separated):
multi-property
Expand Down

0 comments on commit 9608637

Please sign in to comment.