Skip to content

Commit

Permalink
Reduce object-bits for test to avoid OOM (#3511)
Browse files Browse the repository at this point in the history
Kani often runs out of memory on
`tests/expected/function-contract/history/stub.rs` when running the
regressions. In particular, `quadruple_harness` consumes over 9 GB of
memory. This PR reduces the object bits for this test to 8 to avoid OOM
issues. This brings down memory usage to ~125 MB.

Before:
```bash
$ /usr/bin/time -v kani -Zfunction-contracts stub.rs --harness quadruple_harness
        Maximum resident set size (kbytes): 9136036
```

After:
```bash
$ /usr/bin/time -v kani -Zfunction-contracts stub.rs --harness quadruple_harness --enable-unstable --cbmc-args --object-bits 8
...
        Maximum resident set size (kbytes): 125172
```

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
  • Loading branch information
zhassan-aws committed Sep 9, 2024
1 parent 80a4e51 commit 5f6de6e
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion tests/expected/function-contract/history/stub.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
// kani-flags: -Zfunction-contracts
// This test consumes > 9 GB of memory with 16 object bits. Reducing the number
// of object bits to 8 to avoid running out of memory.
// kani-flags: -Zfunction-contracts --enable-unstable --cbmc-args --object-bits 8

#[kani::ensures(|result| old(*ptr + *ptr) == *ptr)]
#[kani::requires(*ptr < 100)]
Expand Down

0 comments on commit 5f6de6e

Please sign in to comment.