Copy-on-write optimization in apron_domains, split_dbm, and sparse_dbm seems flaky
caballa opened this issue · 0 comments
caballa commented
I noticed some cases with split_dbm and sparse_dbm where the analysis does not converge because one of the widening operands is wrong due to COW. For now, I decide to disable COW but with some time I should revisit it and fix it.
For future debugging (it requires to use crab-llvm)
crabllvm ./simple_array_index_value_true-unreach-call4_true-termination.pp.bc --crab-turn-undef-nondet --crab-lower-select --crab-dom=zones --crab-inter-sum-dom=zones --crab-widening-delay=2 --crab-widening-jump-set=0 --crab-narrowing-iterations=2 --crab-relational-threshold=10000 --crab-track=arr --crab-singleton-aliases --crab-add-invariants=none --crab-check=assert --crab-stats