seahorn/crab

zones with bignum seems to be imprecise for computing summaries

Closed this issue · 1 comments

The tests

  • simple/test-arr-4.c
  • simple/test-arr-4.unsafe.c
  • simple/fntest-1.c
  • simple/fntest-1.unsafe.c

from crab-llvm do not pass if we use:

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

in include/crab_llvm/crab_domains.hh

Fixed in commit 85330f0