Cppcheck-2.0 soon

[Daniel Marjamäki]

Our plan right now is to release Cppcheck-2.0 on sunday.

[versat]

The download links on http://cppcheck.net/ still lead to the binaries for version 1.90 instead of 2.0.

[orbitcowboy]

I tried to compile version 2.0 with Z3 as described in the release message, but i am getting compiler errors. The new dependency "libz3-dev" is already installed in my Linux box.
Here is what i get:

$ make USE_Z3=yes 
g++ -Ilib -isystem externals -isystem externals/simplecpp -isystem externals/tinyxml -DUSE_Z3  -pedantic -Wall -Wextra -Wcast-qual -Wno-deprecated-declarations -Wfloat-equal -Wmissing-declarations -Wmissing-format-attribute -Wno-long-long -Wpacked -Wredundant-decls -Wundef -Wno-shadow -Wno-missing-field-initializers -Wno-missing-braces -Wno-sign-compare -Wno-multichar -D_GLIBCXX_DEBUG -g -std=c++0x  -c -o lib/exprengine.o lib/exprengine.cpp
lib/exprengine.cpp: In member function ‘z3::expr ExprData::getExpr(ExprEngine::ValuePtr)’:
lib/exprengine.cpp:843:71: error: call of overloaded ‘int_val(long long int)’ is ambiguous
  843 |                 return context.int_val((long long)(intRange->minValue));
      |                                                                       ^
In file included from lib/exprengine.cpp:144:
/usr/include/z3++.h:2918:17: note: candidate: ‘z3::expr z3::context::int_val(int)’
 2918 |     inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
      |                 ^~~~~~~
/usr/include/z3++.h:2919:17: note: candidate: ‘z3::expr z3::context::int_val(unsigned int)’
 2919 |     inline expr context::int_val(unsigned n) { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
      |                 ^~~~~~~
/usr/include/z3++.h:2920:17: note: candidate: ‘z3::expr z3::context::int_val(int64_t)’
 2920 |     inline expr context::int_val(int64_t n) { Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
      |                 ^~~~~~~
/usr/include/z3++.h:2921:17: note: candidate: ‘z3::expr z3::context::int_val(uint64_t)’
 2921 |     inline expr context::int_val(uint64_t n) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
      |                 ^~~~~~~
make: *** [Makefile:499: lib/exprengine.o] Error 1

[Daniel Marjamäki]

@ettlmartin please compile with NEW_Z3 defined.

make USE_Z3=yes CPPFLAGS="-DUSE_Z3 -DNEW_Z3" .....

I wish we could avoid that #ifdef in our code and make it more intelligent somehow.

[orbitcowboy]

Thanks! But this does not work, i am getting another compiler error:

make USE_Z3=yes CPPFLAGS="-DUSE_Z3 -DNEW_Z3" 
g++ -Ilib -isystem externals -isystem externals/simplecpp -isystem externals/tinyxml -DUSE_Z3 -DNEW_Z3  -pedantic -Wall -Wextra -Wcast-qual -Wno-deprecated-declarations -Wfloat-equal -Wmissing-declarations -Wmissing-format-attribute -Wno-long-long -Wpacked -Wredundant-decls -Wundef -Wno-shadow -Wno-missing-field-initializers -Wno-missing-braces -Wno-sign-compare -Wno-multichar -D_GLIBCXX_DEBUG -g -std=c++0x  -c -o lib/exprengine.o lib/exprengine.cpp
lib/exprengine.cpp: In member function ‘z3::expr ExprData::getExpr(const ExprEngine::BinOpResult*)’:
lib/exprengine.cpp:808:24: error: could not convert ‘(((int)op1.z3::expr::<anonymous>.z3::ast::operator bool()) % ((int)op2.z3::expr::<anonymous>.z3::ast::operator bool()))’ from ‘int’ to ‘z3::expr’
  808 |             return op1 % op2;
      |                    ~~~~^~~~~
      |                        |
      |                        int
make: *** [Makefile:499: lib/exprengine.o] Error 1

[Daniel Marjamäki]

I don't know.. the code is:

#ifdef NEW_Z3
            return op1 % op2;
#else
            return op1 - (op1 / op2) * op2;
#endif

Does it work with the "old" code?

It seems they are actively changing the API :-(

Maybe we should somehow start using a specific z3 version.

[Daniel Marjamäki]

z3 does not officially have version macros as far as I know.. but it might be possible to add something in Cppcheck. Then instead of using some magic "NEW_Z3" macro that could be changed later you could use "Z3_4_8" or something.

[Daniel Marjamäki]

If you compile and run this program does it show some interesting info?

#include <iostream>
#include <z3++.h>

#ifndef Z3_MAJOR_VERSION
#define Z3_MAJOR_VERSION 0
#endif
#ifndef Z3_MINOR_VERSION
#define Z3_MINOR_VERSION 0
#endif
#ifndef Z3_BUILD_NUMBER
#define Z3_BUILD_NUMBER 0
#endif

int main() {
    std::cout << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << std::endl;
    return 0;
}

[orbitcowboy]

Thanks, Obviously the version cannot be detected properly:

g++ test.cpp && ./a.out 
0.0.0

According to apt (package information) there is libz3-dev (4.8.4-1build1) installed.

[Daniel Marjamäki]

my mistake.. it seems we have to include the file z3_version.h. you probably have that but I don't so I will get a compile error :-(.
we could have a default z3_version.h in externals but I would really prefer that it looks in system paths first.

[Daniel Marjamäki]

I think there should be minimum trouble when newer z3 is used. I have an old outdated z3 version and should accept some troubles.

If we #include z3_version.h in Cppcheck then if you have a newer z3 it will work much better. I will get a compile error but I can add my own z3_version.h manually in externals to solve that.

[orbitcowboy]

Thanks. After adding z3_version.h the version is detected properly:

$ g++ test.cpp && ./a.out 
4.8.4

[Daniel Marjamäki]

Can you compile Cppcheck now?

[orbitcowboy]

After updating today make USE_Z3=yes works fine on my side. Thanks!