gernst / legion-symcc

Fresh implementation of the Legion algorithm on top of SyMCC
Other
0 stars 1 forks source link

[TestComp-2022] Invalid trace #25

Open DonggeLiu opened 2 years ago

DonggeLiu commented 2 years ago

Issue

Legion-SymCC reported multiple invalid traces in its output. That invalid trace is extremely long, maybe that is the cause of Z3 parser error? TestCov reported very low coverage (<10%) on this case.

Sample output from Legion-SymCC

?                                  input: 
return code:  -9
< 0
+ 0
? 1                                input: e8acc038
return code:  -9
< 10
+ 0
? 1                                input: bcf20000
return code:  -14
invalid trace ('Z3 parser error', '(assert (bvsgt (concat ...(extremely long trace) ')
? 1                                input: a9971529
return code:  -9

Command

./legion.sh -L ubuntu2004/lib -m 10000 -32 ../../sv-benchmarks/c/array-tiling/poly2.c

Corresponding programs

array-tiling/poly1.yml array-tiling/poly2.yml