gernst / legion-symcc

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

Main change: get rid of `is_exhausted` and `is_explored` #22

Closed gernst closed 2 years ago

DonggeLiu commented 2 years ago

Note sure if the following case is related to resolving this issue

Sample output from Legion-SymCC

?                                  input: 
return code:  -9
< 0
+ 0
? 1                                input: 9478ff55
return code:  -9
< 10
+ 0
e 1                               
? 1                                input: 4bf7100d
return code:  -9
< 10
! 0
? 1                                input: 7d4f1e45
return code:  -9
< 10
! 0
exhausted phantom node in select
this can occur due to max trace length
e 1                               
explored
done

final tree
      local      subtree
   win  try     win  try    path
*    1    1       2    5    
$    0    0       0    0    0
E    1    3       1    4    1

Command

./legion.sh -L ubuntu2004/lib -m 10000 -32 ../../sv-benchmarks/c/loops/nec40.c

Sample program

loops/nec40.yml

gernst commented 2 years ago

done in branch no-exhaust