Skip to content

Commit

Permalink
Website: new post on fixing bottlenecks
Browse files Browse the repository at this point in the history
  • Loading branch information
Alastair Reid committed May 19, 2021
1 parent 96a291f commit 29d6dd2
Showing 1 changed file with 4 additions and 2 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -86,8 +86,6 @@ macro_rules! coherent {
To test these, I wrote a small test to create an array, set each
element of the array to a symbolic value

**todo: check that this matches the latest version of the test and add a link to the actual code**

``` rust
use verification_annotations::prelude::*;

Expand Down Expand Up @@ -118,12 +116,16 @@ fn test_merged() {

Running this test on KLEE with

``` sh
cargo verify --backend=klee --tests -vv --backend-flags=--use-merge |& grep 'generated tests'
```

should result in

```
test_original: {"generated tests": 1024, "total instructions": 709566, "completed paths": 4093}
test_merged: {"generated tests": 1, "completed paths": 41, "total instructions": 11852}
```

Indicating that the original version suffers from a path explosion and generates
more tests, executes more instructions and explores more paths than the merged version.
Expand Down

0 comments on commit 29d6dd2

Please sign in to comment.