search

izlatkin / HornLauncher

scripts and reports for executions seahorn and test generation
0 stars 0 forks source link

[Segmentation fault: 11] for insertion_sort-1.smt2 #13

Closed izlatkin closed 2 years ago

izlatkin commented 3 years ago

tg tool returns Segmentation fault: 11 for file https://github.com/sosy-lab/sv-benchmarks/blob/master/c/loops/insertion_sort-1.c

/Users/ilyazlatkin/PycharmProjects/aeval/build/tools/tg/tg --keys 19641,6306 insertion_sort-1.smt2

$ /Users/ilyazlatkin/PycharmProjects/aeval/build/tools/tg/tg --keys 19641,6306 insertion_sort-1.smt2 outgs from main@_shadow.mem.0.0: (0) -> main@_shadow.mem.0.1 (3) -> main@_shadow.mem.0.0 outgs from main@_shadow.mem.0.1: (1) -> main@_ret (4) -> main@_shadow.mem.0.2 outgs from main@_shadow.mem.0.2: (2) -> main@_20 (5) -> main@_shadow.mem.0.1 outgs from main@_20: (6) -> main@_shadow.mem.0.1 (8) -> main@_shadow.mem.0.2 ARRCAND FROM DATA 1: ((_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))=0) ARRCAND FROM DATA 1: ([+ _FH_3 _FH_5 -select(_FH_1, _FH_0+(4*_FH_2))]=0) ARRCAND FROM DATA 1: ([+ -_FH_3 select(_FH_1, _FH_0+(4*_FH_2)) _FH_5]=0) ARRCAND FROM DATA 1: (_FH_5=(_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))) ARRCAND FROM DATA 1: (_FH_5=((-_FH_3)+select(_FH_1, _FH_0+(4*_FH_2)))) ARRCAND FROM DATA 1: ([+ _FH_2 _FH_3 -select(_FH_1, _FH_0+(4*_FH_2))]=1) ARRCAND FROM DATA 2: ((_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))=0) ARRCAND FROM DATA 1: ([+ _FH_3 -select(_FH_1, _FH_0+(4*_FH_2)) -_FH_2]=-1) ARRCAND FROM DATA 2: ([+ _FH_3 -_FH_2 -select(_FH_1, _FH_0+(4*_FH_2))]=(-1*_FH_2)) ARRCAND FROM DATA 1: ((_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))=(_FH_2+-1)) ARRCAND FROM DATA 1: ((_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))=((-_FH_2)+1)) ARRCAND FROM DATA 1: ([+ _FH_2 _FH_3 -select(_FH_1, _FH_0+(4*_FH_2))]=_FH_4) ARRCAND FROM DATA 1: ([+ _FH_3 -select(_FH_1, _FH_0+(4*_FH_2)) -_FH_2]=(-_FH_4)) ARRCAND FROM DATA 1: ([+ _FH_3 _FH_4 -select(_FH_1, _FH_0+(4*_FH_2))]=_FH_2) ARRCAND FROM DATA 1: ([+ _FH_3 -select(_FH_1, _FH_0+(4*_FH_2)) -_FH_4]=(-_FH_2)) ARRCAND FROM DATA 1: ((_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))=0) ARRCAND FROM DATA 1: ([+ _FH_3 _FH_5 -select(_FH_1, _FH_0+(4*_FH_2))]=0) ARRCAND FROM DATA 1: ([+ -_FH_3 select(_FH_1, _FH_0+(4*_FH_2)) _FH_5]=0) ARRCAND FROM DATA 1: (_FH_5=(_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))) ARRCAND FROM DATA 1: (_FH_5=((-_FH_3)+select(_FH_1, _FH_0+(4*_FH_2)))) ARRCAND FROM DATA 1: ([+ _FH_2 _FH_3 -select(_FH_1, _FH_0+(4*_FH_2))]=1) ARRCAND FROM DATA 2: ((_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))=0) ARRCAND FROM DATA 2: ([+ _FH_2 _FH_3 -select(_FH_1, _FH_0+(4*_FH_2))]=_FH_4) ARRCAND FROM DATA 1: ([+ _FH_3 -select(_FH_1, _FH_0+(4*_FH_2)) -_FH_2]=-1) ARRCAND FROM DATA 2: ([+ _FH_3 -_FH_2 -select(_FH_1, _FH_0+(4*_FH_2))]=(-1*_FH_2)) ARRCAND FROM DATA 2: ([+ _FH_3 -_FH_2 -select(_FH_1, _FH_0+(4*_FH_2))]=(-1*_FH_4)) ARRCAND FROM DATA 1: ((_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))=(_FH_2+-1)) ARRCAND FROM DATA 1: ((_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))=((-_FH_2)+1)) ARRCAND FROM DATA 1: ([+ _FH_2 _FH_3 -select(_FH_1, _FH_0+(4*_FH_2))]=_FH_4) ARRCAND FROM DATA 1: ([+ _FH_3 -select(_FH_1, _FH_0+(4*_FH_2)) -_FH_2]=(-_FH_4)) ARRCAND FROM DATA 1: ([+ _FH_3 _FH_4 -select(_FH_1, _FH_0+(4*_FH_2))]=_FH_2) ARRCAND FROM DATA 1: ([+ _FH_3 -select(_FH_1, _FH_0+(4*_FH_2)) -_FH_4]=(-_FH_2)) ARRCAND FROM DATA 1: ([+ _FH_2 _FH_3 _FH_5 -select(_FH_1, _FH_0+(4*_FH_2))]=1) ARRCAND FROM DATA 2: ([+ _FH_3 _FH_5 -select(_FH_1, _FH_0+(4*_FH_2))]=0) ARRCAND FROM DATA 2: ([+ _FH_2 _FH_3 _FH_5 -select(_FH_1, _FH_0+(4*_FH_2))]=_FH_4) ARRCAND FROM DATA 1: ([+ _FH_3 -select(_FH_1, _FH_0+(4*_FH_2)) -_FH_2 -_FH_5]=-1) ARRCAND FROM DATA 2: ([+ _FH_3 -_FH_5 -_FH_2 -select(_FH_1, _FH_0+(4*_FH_2))]=(-1*_FH_2)) ARRCAND FROM DATA 2: ([+ _FH_3 -_FH_5 -_FH_2 -select(_FH_1, _FH_0+(4*_FH_2))]=(-1*_FH_4)) ARRCAND FROM DATA 1: ((_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))=[+ _FH_2 _FH_5 -1]) ARRCAND FROM DATA 1: ((_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))=[+ -_FH_2 -_FH_5 1]) ARRCAND FROM DATA 1: ([+ _FH_3 _FH_5 -select(_FH_1, _FH_0+(4*_FH_2)) -1*_FH_2]=-1) ARRCAND FROM DATA 2: ([+ _FH_3 _FH_5 -select(_FH_1, _FH_0+(4*_FH_2))]=0) ARRCAND FROM DATA 2: ([+ _FH_3 _FH_5 -select(_FH_1, _FH_0+(4*_FH_2)) -1*_FH_2]=(-1*_FH_4)) ARRCAND FROM DATA 1: ([+ _FH_3 -select(_FH_1, _FH_0+(4*_FH_2)) -_FH_5 _FH_2]=-1) ARRCAND FROM DATA 2: ([+ _FH_2 _FH_3 -_FH_5 -select(_FH_1, _FH_0+(4*_FH_2))]=(-1*_FH_2)) ARRCAND FROM DATA 2: ([+ _FH_2 _FH_3 -_FH_5 -select(_FH_1, _FH_0+(4*_FH_2))]=(-1*_FH_4)) ARRCAND FROM DATA 1: ((_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))=[+ _FH_5 -1*_FH_2 1]) ARRCAND FROM DATA 1: ((_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))=[+ -_FH_5 _FH_2 -1]) ARRCAND FROM DATA 1: ([+ _FH_2 _FH_3 _FH_5 -select(_FH_1, _FH_0+(4*_FH_2)) -1*_FH_4]=0) ARRCAND FROM DATA 1: ([+ _FH_3 -select(_FH_1, _FH_0+(4*_FH_2)) -_FH_2 -_FH_5 _FH_4]=0) ARRCAND FROM DATA 1: ((_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))=[+ _FH_2 _FH_5 -1*_FH_4]) ARRCAND FROM DATA 1: ((_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))=[+ -_FH_2 -_FH_5 _FH_4]) ARRCAND FROM DATA 1: ([+ _FH_3 _FH_4 _FH_5 -select(_FH_1, _FH_0+(4*_FH_2)) -1*_FH_2]=0) ARRCAND FROM DATA 1: ([+ _FH_3 -select(_FH_1, _FH_0+(4*_FH_2)) -_FH_4 -_FH_5 _FH_2]=0) ARRCAND FROM DATA 1: ((_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))=[+ _FH_4 _FH_5 -1*_FH_2]) ARRCAND FROM DATA 1: ((_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))=[+ -_FH_4 -_FH_5 _FH_2]) ARRCAND FROM DATA 1: ([+ _FH_3 -select(_FH_1, _FH_0+(4*_FH_2)) -1*_FH_4 2*_FH_2]=1) ARRCAND FROM DATA 2: ([+ _FH_3 -select(_FH_1, _FH_0+(4*_FH_2)) -1*_FH_4 2*_FH_2]=_FH_2) ARRCAND FROM DATA 2: ([+ _FH_3 -select(_FH_1, _FH_0+(4*_FH_2)) -1*_FH_4 2*_FH_2]=_FH_4) ARRCAND FROM DATA 1: ([+ _FH_3 -select(_FH_1, _FH_0+(4*_FH_2)) _FH_4 -2*_FH_2]=-1) ARRCAND FROM DATA 2: ([+ _FH_3 _FH_4 -select(_FH_1, _FH_0+(4*_FH_2)) -2*_FH_2]=(-1*_FH_2)) ARRCAND FROM DATA 2: ([+ _FH_3 _FH_4 -select(_FH_1, _FH_0+(4*_FH_2)) -2*_FH_2]=(-1*_FH_4)) ARRCAND FROM DATA 1: ((_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))=[+ -1*_FH_4 2*_FH_2 -1]) ARRCAND FROM DATA 1: ((_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))=[+ _FH_4 -2*_FH_2 1]) ARRCAND FROM DATA 1: ([+ _FH_3 _FH_4 -select(_FH_1, _FH_0+(4*_FH_2))]=1) ARRCAND FROM DATA 2: ([+ _FH_3 _FH_4 -select(_FH_1, _FH_0+(4*_FH_2))]=_FH_2) ARRCAND FROM DATA 2: ((_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))=0) ARRCAND FROM DATA 1: ([+ _FH_3 -select(_FH_1, _FH_0+(4*_FH_2)) -_FH_4]=-1) ARRCAND FROM DATA 2: ([+ _FH_3 -_FH_4 -select(_FH_1, _FH_0+(4*_FH_2))]=(-1*_FH_2)) ARRCAND FROM DATA 2: ([+ _FH_3 -_FH_4 -select(_FH_1, _FH_0+(4*_FH_2))]=(-1*_FH_4)) ARRCAND FROM DATA 1: ((_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))=(_FH_4+-1)) ARRCAND FROM DATA 1: ((_FH_3+(-select(_FH_1, _FH_0+(4*_FH_2))))=((-_FH_4)+1)) Segmentation fault: 11

izlatkin commented 3 years ago

insertion_sort-1.smt2.txt

izlatkin commented 3 years ago

same error for https://github.com/sosy-lab/sv-benchmarks/blob/master/c/loops/insertion_sort-2.c

grigoryfedyukovich commented 3 years ago

It has arrays, which tg does not support.

izlatkin commented 3 years ago

Is tg going to support them ?

izlatkin commented 3 years ago

log.txt

Failed to marshal: (_FH_0=true)
Assertion failed: (res != NULL), function marshal, file /Users/ilyazlatkin/PycharmProjects/aeval/include/ufo/Smt/ZExprConverter.hpp, line 498.
grigoryfedyukovich commented 3 years ago

fixed

izlatkin commented 3 years ago

fixed. Now coverga is Hit: 16 Total: 16 Coverage: 100.0 %

very strange error for test 3

./test-coverage 
Bus error: 10

not clean what is the source of error