Running example with SMACK

[m-carrasco]

Hi,

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.

In a more general sense, should #include <assert.h> be always included? I think this question may be related to #627

Thanks for your time.

Kind regards,
Manuel