diff options
| author |  qunyanm <qunyanm@hotmail.com> | 2015-12-15 11:04:27 -0800 |
|---|---|---|
| committer | qunyanm <qunyanm@hotmail.com> | 2015-12-15 11:04:27 -0800 |
| commit | eb64daf4d3b3609bc47fa8f0f22069e7576c80c7 (patch) | |
| tree | 668923025c0de2a99a4cb2b6ceb2133a014f1ed4 /Test | |
| parent | 277e5e7400330f4b26270fcaa4b0a70514b35104 (diff) | |
| parent | 8938d00be93e780d54917c1448bc534702766fdf (diff) | |
Merge branch 'master' of https://github.com/boogie-org/boogie
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect | 3 | ||||
| -rw-r--r-- | Test/test15/CaptureState.bpl.expect | 18 |
2 files changed, 11 insertions, 10 deletions
diff --git a/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect b/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect index 9f960f26..3c0d0b20 100644 --- a/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect +++ b/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect @@ -127,7 +127,8 @@ Execution trace: daytona_bug2_ioctl_example_2.bpl(3832,3): inline$storm_IoCancelIrp$0$anon10#2 daytona_bug2_ioctl_example_2.bpl(3892,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#2 daytona_bug2_ioctl_example_2.bpl(3902,3): inline$storm_IoAcquireCancelSpinLock$0$anon8_Else#2 - daytona_bug2_ioctl_example_2.bpl(3928,3): inline$storm_IoAcquireCancelSpinLock$0$anon9_Then#2 + daytona_bug2_ioctl_example_2.bpl(3915,3): inline$storm_IoAcquireCancelSpinLock$0$anon9_Else#2 + daytona_bug2_ioctl_example_2.bpl(3923,3): inline$storm_IoAcquireCancelSpinLock$0$anon10_Then#2 daytona_bug2_ioctl_example_2.bpl(3933,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#2 daytona_bug2_ioctl_example_2.bpl(3944,3): inline$storm_IoAcquireCancelSpinLock$0$anon11_Then#2 daytona_bug2_ioctl_example_2.bpl(3949,3): inline$storm_IoAcquireCancelSpinLock$0$anon7#2 diff --git a/Test/test15/CaptureState.bpl.expect b/Test/test15/CaptureState.bpl.expect index 5d9d41c5..6939fee4 100644 --- a/Test/test15/CaptureState.bpl.expect +++ b/Test/test15/CaptureState.bpl.expect @@ -14,17 +14,17 @@ $mv_state_const -> 3 F -> T@FieldName!val!0 Heap -> |T@[Ref,FieldName]Int!val!0| m -> **m -m@0 -> (- 276) -m@1 -> (- 275) -m@3 -> (- 275) +m@0 -> (- 2) +m@1 -> (- 1) +m@3 -> (- 1) r -> **r -r@0 -> (- 550) +r@0 -> (- 2) this -> T@Ref!val!0 x -> 719 y -> **y Select_[Ref,FieldName]$int -> { - |T@[Ref,FieldName]Int!val!0| T@Ref!val!0 T@FieldName!val!0 -> (- 276) - else -> (- 276) + |T@[Ref,FieldName]Int!val!0| T@Ref!val!0 T@FieldName!val!0 -> (- 2) + else -> (- 2) } $mv_state -> { 3 0 -> true @@ -49,13 +49,13 @@ tickleBool -> { *** STATE top *** END_STATE *** STATE then - m -> (- 276) + m -> (- 2) *** END_STATE *** STATE postUpdate0 - m -> (- 275) + m -> (- 1) *** END_STATE *** STATE end - r -> (- 550) + r -> (- 2) m -> 7 *** END_STATE *** END_MODEL |