search

seahorn / crab

A library for building abstract interpretation-based analyses
Apache License 2.0
234 stars 32 forks source link

Possibly stack overflow while computing WTO of a large CFG #18

Closed caballa closed 5 years ago

caballa commented 6 years ago

Problem07_label52_true-unreach-call.pp.bc.zip

Command to reproduce the problem using crab-llvm:

crabllvm Problem07_label52_true-unreach-call.pp.bc --crab-verbose=2 --crab-dom=int --crab-widening-delay=2 --crab-widening-jump-set=0 --crab-narrowing-iterations=2 --crab-track=arr --crab-singleton-aliases --crab-check=assert --crab-stats --crab-disable-warnings

silently produces signal 11 (SEGFAULT). I did some gdb and it seems that we run out of stack while computing WTO using recursion.

caballa commented 5 years ago

This has been fixed in commit e6a5a3c012c1f8ac427ba79cdb7f4d4545afc2f3