Mark S. Baranowski

This PR addresses the following: * Improves path manipulation in `regtest.py` to be more compatible with macOS (based on work by @shaobo-he) * Extends the expected name for `bc` files...

SMACK should be able to check if Rust's allocator is used on memory originating from a different allocator. For example, a pointer from C allocated with `malloc` may be obtained...

SMACK can now support the PhantomData structure from standard Rust, so the model in `smack.rs` is no longer needed.

Currently the following: ```rust fn main() { assert!(0==1); } ``` will pass in SMACK because this generates an assertion failure in the standard library. This should require checking for the...

Smack does not currently model LLVM's `poison` values. These arise as the result of invalid computations. It's not clear what this actually means for verification, however these can arise, for...

We model accesses to aggregate values by adding `load/store` instructions to the IR to match corresponding `store/load` instructions. This requires pointer arithmetic which is later instrumented for checking by the...

Smack does not model LLVM saturation arithmetic instructions

1

https://llvm.org/docs/LangRef.html#saturation-arithmetic-intrinsics This should be pretty easy to implement using the machinery of the IntegerOverflow pass.

IntegerOverflowChecker generates redundant instructions for unsigned intrinsics

4

Currently, instructions like `@llvm.uadd.with.overflow.i32` are translated to approximately: ``` // %res = call {i32, i1} @llvm.uadd.with.overflow.i32(%a, %b) ... $a1 = $zext.i32.i64($a); $a2 = $zext.i32.i64($b); $res = $add.i64($a1, $b1); $over =...

We do not currently handle the `copysign` family of functions. This is due to a limitation of SMT-LIB where `NaN` has a singular representation, whereas C allows numerous representations for...

The version of Boogie we use no longer supports CVC4. This pull request addresses that by updating the installer and SMACK to use CVC5 instead.