Failed overflow-checker assertion in C++ mode.

[michael-emmi]

An assertion in IntegerOverflowChecker fails when compiling in C++ mode:

$ cat a.cpp && smack a.cpp --clang-options="-x c++ -std=c++14"

#include <smack.h>

int main() {
	return 0;
}
SMACK program verifier version 1.9.0
Assertion failed: (co != NULL && "Function __SMACK_check_overflow should be present."), function runOnModule, file /Users/mje/Code/smack/lib/smack/IntegerOverflowChecker.cpp, line 113.
Stack dump:
0.	Program arguments: llvm2bpl /Users/mje/Code/smack/b-gxo6nc.bc -bpl /Users/mje/Code/smack/a-p5MCD_.bpl -warnings -source-loc-syms -entry-points main -mem-mod-impls 
1.	Running pass 'Checked integer arithmetic intrinsics' on module '/Users/mje/Code/smack/b-gxo6nc.bc'.
Traceback (most recent call last):
  File "/usr/local/bin/smack", line 13, in <module>
    smack.top.main()
  File "/usr/local/bin/../share/smack/top.py", line 769, in main
    frontend(args)
  File "/usr/local/bin/../share/smack/top.py", line 285, in frontend
    return frontends()[lang](args)
  File "/usr/local/bin/../share/smack/top.py", line 362, in clang_plusplus_frontend
    default_link_bc_files(compile_command, args)
  File "/usr/local/bin/../share/smack/top.py", line 448, in default_link_bc_files
    llvm_to_bpl(args)
  File "/usr/local/bin/../share/smack/top.py", line 499, in llvm_to_bpl
    try_command(cmd, console=True)
  File "/usr/local/bin/../share/smack/utils.py", line 69, in try_command
    raise Exception(output)
Exception: Assertion failed: (co != NULL && "Function __SMACK_check_overflow should be present."), function runOnModule, file /Users/mje/Code/smack/lib/smack/IntegerOverflowChecker.cpp, line 113.
Stack dump:
0.	Program arguments: llvm2bpl /Users/mje/Code/smack/b-gxo6nc.bc -bpl /Users/mje/Code/smack/a-p5MCD_.bpl -warnings -source-loc-syms -entry-points main -mem-mod-impls 
1.	Running pass 'Checked integer arithmetic intrinsics' on module '/Users/mje/Code/smack/b-gxo6nc.bc'.

This is a simplified version of michael-emmi/ctverif#2.

[niekbouman]

Hi Michael (and/or others),

I managed to get rid of this error by adding a missing function declaration in smack.h:

void __SMACK_check_overflow(int);

Now I am facing another issue, related to

smack_value_t __SMACK_value()

whose declaration I have (as a hack) changed into

smack_value_t __SMACK_value(int)

since C++ does not support C-style functions with unspecified number of arguments.

Now I get an error in SmackRep.cpp, namely the Unexpected argument type error at line 406 of SmackRep.cpp...

[michael-emmi]

Hi @niekbouman the issue of the __SMACK_value API for C++ code is independent from the overflow -checking code, so let’s please raise it as a separate issue.

[niekbouman]

Good idea, I've added it as issue 353.

[zvonimir]

When I run this same command on my machine, I get a different error:

SMACK program verifier version 1.9.0
Traceback (most recent call last):
  File "/home/zvonimir/projects/smack-project/smack/install/bin/smack", line 13, in <module>
    smack.top.main()
  File "/home/zvonimir/projects/smack-project/smack/install/bin/../share/smack/top.py", line 769, in main
    frontend(args)
  File "/home/zvonimir/projects/smack-project/smack/install/bin/../share/smack/top.py", line 285, in frontend
    return frontends()[lang](args)
  File "/home/zvonimir/projects/smack-project/smack/install/bin/../share/smack/top.py", line 362, in clang_plusplus_frontend
    default_link_bc_files(compile_command, args)
  File "/home/zvonimir/projects/smack-project/smack/install/bin/../share/smack/top.py", line 447, in default_link_bc_files
    try_command(['llvm-link', '-o', args.linked_bc_file, args.bc_file] + build_libs(args))
  File "/home/zvonimir/projects/smack-project/smack/install/bin/../share/smack/top.py", line 333, in build_libs
    try_command(default_clang_compile_command(args, True) + ['-o', bc, c])
  File "/home/zvonimir/projects/smack-project/smack/install/bin/../share/smack/utils.py", line 69, in try_command
    raise Exception(output)
Exception: In file included from /home/zvonimir/projects/smack-project/smack/install/share/smack/lib/smack.c:7:
/usr/include/stdlib.h:543:13: error: exception specification in declaration does not match previous declaration
extern void exit (int __status) __THROW __attribute__ ((__noreturn__));
            ^
/home/zvonimir/projects/smack-project/smack/install/share/smack/include/smack.h:57:6: note: previous declaration is here
void exit(int);

It seems that the problem is related to the fact that C and C++ have slightly different signatures for common standard library functions, such as exit. We should probably have (somewhat) separate C and C++ headers. This pull request is a step in that direction: #348
Thoughts?

[niekbouman]

I've opened a new issue for this exit related problem; see 359

[michael-emmi]

Shouldn’t we just add the following declaration to <smack.h>?

void __SMACK_check_overflow(int);

[zvonimir]

Yes, I agree we should add __SMACK_check_overflow declaration to smack.h.