Michael Emmi
Michael Emmi
Currently smack is translating reads of uninitilized variables to reads of an $UNDEF constant. This is not ideal, since to be sound, distinct uninitialized variables need not be equal, i.e.,...
It would be great to have build artifacts (binaries) uploaded with each release, i.e., automated with Travis. Particularly: * RedHat/Yum * Ubuntu/Apt * MacOS/Homebrew Maybe we could start with creating...
The following program is apparently not well defined by the C standard due to the type-unsafe call. However, real compilers end up actually calling `foo` and thus lead to an...
e.g. when we encounter an inline assembly call. One idea would be to have a warning system: generate the Boogie code, and signal to the user that certain code is...
The documentation should address the most basic concerns about running Smack, including loops and (bounded) unrolling, assertions, assumptions, and nondeterministic inputs. One approach would be to start with a very...
An assertion in IntegerOverflowChecker fails when compiling in C++ mode: ``` $ cat a.cpp && smack a.cpp --clang-options="-x c++ -std=c++14" #include int main() { return 0; } SMACK program verifier...
This probably boils down to an issue with Corral, but I thought I’d post here first in case there’s some issue with the way we’re invoking Corral. ```console % cat...
Seems that contract extraction fails when loop heads contain non-atomic terms: ```console % cat loop_with_expr.c && echo -- && smack loop_with_expr.c #include #include void foo(int i) { while (i &&...
Counterexample traces can be hard to reason about, since we see only a limited view of the program values along a given path. Ideally, wouldn’t it be great to fire...
It should be more obvious that Smack could not make any conclusions when compiling the given analysis target fails. Consider what currently happens: ``` $ smack main.c SMACK program verifier...