CRAB error because GMP z_number does not fit into a signed long integer

[caballa]

CRAB ERROR: mpz_class -9223372036854775809 does not fit into a signed long integer

This happens with split-dbm domain. This is a well known limitation since the domain uses for efficiency signed long integer as DBM weights rather than unlimited precision z_number.

Attached a zip file to reproduce the problem:

split-dbm-too-big-weight.zip

[caballa]

The solution to avoid this problem is to change in include/crab_domains.hh:

typedef SDBM_impl::DefaultParams<number_t> SplitDBMGraph; typedef SplitDBM<number_t, varname_t, SplitDBMGraph> BASE(split_dbm_domain_t);
with

typedef SDBM_impl::BigNumDefaultParams<number_t> SplitDBMGraph; typedef SplitDBM<number_t, varname_t, SplitDBMGraph> BASE(split_dbm_domain_t);
This will use bignums as graph weights.

[caballa]

Since LLVM 5.0 this problem should be gone. First, it seems that Clang/LLVM 5.0 does not produce such a large numbers. Second, we have added an option --crab-enable-bignums which is false by default. If this option is false, the translation from LLVM bitcode to crab havocs any operation whose operand cannot be represented as a signed integer in 64 bits.