cuplv / verivita

Dynamic verification using callbacks
2 stars 1 forks source link

Trace simulation bug #142

Closed ftc closed 7 years ago

ftc commented 7 years ago

command: python driver.py -m simulate -t trace_150117_0 -s /home/s/Documents/source/callback-verification/cbverifier/android_specs/enabledisable/android.view.View/button_attachdetach_setListener.spec -z -w 6464

exception:

Traceback (most recent call last):
  File "/home/s/Documents/source/callback-verification/cbverifier/driver.py", line 335, in <module>
    main()
  File "/home/s/Documents/source/callback-verification/cbverifier/driver.py", line 301, in main
    (steps, cex, mapback) = driver.run_simulation(cb_sequence)
  File "/home/s/Documents/source/callback-verification/cbverifier/driver.py", line 120, in run_simulation
    trace_enc = ts_enc.get_trace_encoding(cb_sequence)
  File "/home/s/Documents/source/callback-verification/cbverifier/encoding/encoder.py", line 288, in get_trace_encoding
    msg_enc = self.mapback.get_trans2pc((entry_type, msg))
UnboundLocalError: local variable 'entry_type' referenced before assignment

Process finished with exit code 1

files: bug.zip

ftc commented 7 years ago

Sorry but this was with running it on all of the specs: -s /home/s/Documents/source/callback-verification/cbverifier/android_specs/enabledisable/android.view.View/button_attachdetach_setListener.spec:/home/s/Documents/source/callback-verification/cbverifier/android_specs/enabledisable/android.os.CountdownTimer/countdowntimer.spec:/home/s/Documents/source/callback-verification/cbverifier/android_specs/enabledisable/android.app.Fragment/Fragment.spec:/home/s/Documents/source/callback-verification/cbverifier/android_specs/allowdisallow/fragment/fragment_getString.spec

These should all be in the git repo under fragment_specs

ftc commented 7 years ago

with all specs: bug.zip