search

gernst / legion-symcc

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

[TestComp-2022] Assertion Error (line 254) #15

Closed DonggeLiu closed 2 years ago

DonggeLiu commented 2 years ago

Legion-SymCC terminated on many benchmarking programs because of assertion error in line 254:

Traceback (most recent call last):
  File "Legion.py", line 825, in <module>
    raise e
  File "Legion.py", line 730, in <module>
    root.check_invariants()
  File "Legion.py", line 261, in check_invariants
    raise e
  File "Legion.py", line 257, in check_invariants
    self.yes.check_invariants()
  File "Legion.py", line 261, in check_invariants
    raise e
  File "Legion.py", line 258, in check_invariants
    self.no.check_invariants()
  File "Legion.py", line 261, in check_invariants
    raise e
  File "Legion.py", line 257, in check_invariants
    self.yes.check_invariants()
  File "Legion.py", line 261, in check_invariants
    raise e
  File "Legion.py", line 258, in check_invariants
    self.no.check_invariants()
  File "Legion.py", line 261, in check_invariants
    raise e
  File "Legion.py", line 257, in check_invariants
    self.yes.check_invariants()
  File "Legion.py", line 261, in check_invariants
    raise e
  File "Legion.py", line 257, in check_invariants
    self.yes.check_invariants()
  File "Legion.py", line 261, in check_invariants
    raise e
  File "Legion.py", line 257, in check_invariants
    self.yes.check_invariants()
  File "Legion.py", line 261, in check_invariants
    raise e
  File "Legion.py", line 257, in check_invariants
    self.yes.check_invariants()
  File "Legion.py", line 261, in check_invariants
    raise e
  File "Legion.py", line 254, in check_invariants
    assert self.yes.is_explored
AssertionError

Corresponding programs include (but are not limited to):

  1. heap-manipulation/dancing.yml
  2. loops/trex02-2.yml
  3. verifythis/tree_del_iter_incorrect.yml
  4. verifythis/tree_del_rec_incorrect.yml
  5. seq-mthreaded/pals_floodmax.3.1.ufo.BOUNDED-6.pals.yml
  6. seq-mthreaded/pals_floodmax.3.2.ufo.BOUNDED-6.pals.yml
  7. seq-mthreaded/pals_floodmax.3.2.ufo.UNBOUNDED.pals.yml
  8. seq-mthreaded/pals_floodmax.3.3.ufo.BOUNDED-6.pals.yml
  9. seq-mthreaded/pals_floodmax.3.4.ufo.BOUNDED-6.pals.yml ...
  10. seq-mthreaded/pals_opt-floodmax.5.ufo.BOUNDED-10.pals.yml
DonggeLiu commented 2 years ago

Command: ./legion.sh -L ubuntu2004/lib -m 10000 -32 ../../sv-benchmarks/c/seq-mthreaded/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c