I successfully created an interactive docker container following the documentation. However, I ran into some problems when testing this example.
user@555c547b444f:~/smack$ smack examples/rise4fun/rise_simple_buggy.c
SMACK program verifier version 2.8.0
examples/rise4fun/rise_simple_buggy.c:9:3: warning: implicit declaration of function 'assert' is invalid in C99 [-Wimplicit-function-declaration]
assert(z != 30);
^
1 warning generated.
SMACK found no errors with unroll bound 1.
Is this the expected behaviour?
Adding #include <assert.h> solves this problem, and the assertion violation is detected.
user@555c547b444f:~/smack$ smack examples/rise4fun/rise_simple_buggy.c
SMACK program verifier version 2.8.0
/usr/local/share/smack/lib/smack.c(1885,3):
/usr/local/share/smack/lib/smack.c(1890,1):
examples/rise4fun/rise_simple_buggy.c(9,9): smack:entry:main = -1032, z = 30
examples/rise4fun/rise_simple_buggy.c(10,3): CALL __VERIFIER_assert
/usr/local/share/smack/lib/smack.c(1606,29): __VERIFIER_assert:arg:x = 0
/usr/local/share/smack/lib/smack.c(52,3):
examples/rise4fun/rise_simple_buggy.c(10,3): RETURN from __VERIFIER_assert
SMACK found an error.
If the header is missing from the file, I am more than willing to open a MR and fix it.
Hi,
I successfully created an interactive docker container following the documentation. However, I ran into some problems when testing this example.
Is this the expected behaviour?
Adding
#include <assert.h>
solves this problem, and the assertion violation is detected.If the header is missing from the file, I am more than willing to open a MR and fix it.
In a more general sense, should
#include <assert.h>
be always included? I think this question may be related to https://github.com/smackers/smack/pull/627Thanks for your time.
Kind regards, Manuel