cuplv / verivita

Dynamic verification using callbacks
2 stars 1 forks source link

Stuck on fixing a simulation issue #212

Open ftc opened 6 years ago

ftc commented 6 years ago

The trace is in the following zip file: simulation_block.zip

The specifications I am running it with are as follows. They are in the branch va1_big_sim_fix of callback-verification.

/Users/s/Documents/source/callback-verification/cbverifier/android_specs/enabledisable/android.app.Fragment/DialogFragment_lifecycle.spec:/Users/s/Documents/source/callback-verification/cbverifier/android_specs/enabledisable/android.view.View/v iew_REGEX.spec:/Users/s/Documents/source/callback-verification/cbverifier/android_specs/enabledisable/android.os.CountdownTimer/countdowntimer.spec:/Users/s/Documents/source/callback-verification/cbverifier/android_specs/enabledisable/android.app.Fragment/Fragment.spec:/Users/s/Documents/source/callback-verification/cbverifier/android_specs/enabledisable/android.view.View/onClick_listener_setenabled.spec:/Users/s/Documents/source/callback-verification/cbverifier/android_specs/enable$isable/android.os.AsyncTask/AsyncTask.spec:/Users/s/Documents/source/callback-verification/cbverifier/android_specs/enabledisable/android.app.Activity/activity_lifestate.spec:/Users/s/Documents/source/callback-verification/cbverifier/android_s$ecs/subexpr/android.app.AlertDialog/dialog.spec:/Users/s/Documents/source/callback-verification/cbverifier/android_specs/enabledisable/android.app.AlertDialog/DialogInterfaces_OnClickListener.spec:/Users/s/Documents/source/callback-verificatio$/cbverifier/android_specs/subexpr/android.widget.PopupMenu/popupmenu.spec:/Users/s/Documents/source/callback-verification/cbverifier/android_specs/enabledisable/android.widget.PopupMenu/PopupMenu.spec:/Users/s/Documents/source/callback-verific$tion/cbverifier/android_specs/subexpr/android.widget.Toolbar/toolbar.spec:/Users/s/Documents/source/callback-verification/cbverifier/android_specs/enabledisable/android.widget.Toolbar/onMenuItemClick.spec:/Users/s/Documents/source/callback-ver$fication/cbverifier/android_specs/subexpr/android.app.Activity/activity_callbacks.spec:/Users/s/Documents/source/callback-verification/cbverifier/android_specs/subexpr/android.app.Fragment/fragment_callbacks.spec:/Users/s/Documents/source/call$ack-verification/cbverifier/android_specs/subexpr/android.app.Activity/activity_aux.spec

From my debugging so far you can remove any one of the following spec files and be able to simulate: activity_lifestate.spec Fragment.spec onClick_listener_setenabled.spec

Removing one of the following spec files does not make the trace simulate countdowntimer.spec DialogFragment_lifecycle AsyncTask.spec