(* created : Thu Nov 19 15:55:37 CET 2009 *) # # This file was generated by PSEUDO # which is copyright (C) 2009 Universitaet Karlsruhe, Germany # written by Mattias Ulbrich # include "$bytecode.p" "$decproc.p" properties BreakpointStrategy.stopAtLoop "false" (* Database declarations *) (* Program declarations *) function (* local variables *) ref _this assignable field(int) field_Zune_days unique field(int) field_Zune_year unique (* Program *) program P source "Zune.java" assume sel(h, _this, created) & !_this = null assume sel(h, _this, field_Zune_days) >= 0 assume sel(h, _this, field_Zune_year) >= 1980 assume true stmt0: sourceline 14 (* 0: aload_0[42](1) *) skip_loopinv (* invariant *) sel(h, _this, field_Zune_days) >= 0 & sel(h, _this, field_Zune_year) >= 1980, (* variant *) sel(h, _this, field_Zune_days) st := push(st, _this) stmt1: sourceline 14 (* 1: getfield[180](3) 3 *) assert !topRef(st) = null ; "non-null field access receiver" st := push(pop(st), sel(h, topRef(st), field_Zune_days)) stmt4: sourceline 14 (* 4: sipush[17](3) 365 *) st := push(st, 365) stmt7: sourceline 14 (* 7: if_icmple[164](3) -> return *) goto branch0, branch1 branch0: assume top2Int(st) <= topInt(st) st := pop2(st) goto stmt86 branch1: assume !top2Int(st) <= topInt(st) st := pop2(st) stmt10: sourceline 16 (* 10: ldc[18](2) 4 *) skip stmt15: sourceline 20 (* 15: aload_0[42](1) *) st := push(st, _this) stmt16: sourceline 20 (* 16: aload_0[42](1) *) st := push(st, _this) stmt17: sourceline 20 (* 17: getfield[180](3) 2 *) assert !topRef(st) = null ; "non-null field access receiver" st := push(pop(st), sel(h, topRef(st), field_Zune_year)) stmt20: sourceline 20 (* 20: invokevirtual[182](3) 6 *) assert !top2Ref(st) = null ; "non-null method receiver" assert topInt(st) > 0 ; "establish pre condition" havoc anon havoc boolRet h := disturb(h, anon, nothing) assume exc = null; "assume post condition" st := pop(st) goto excHnd0, excHnd1 excHnd0: assume !exc = null ; "Exception raised" st := push(st, exc) goto end_of_proc ; "Propagate exception" excHnd1: assume exc = null ; "No exception" st := push(st, boolRet) stmt23: sourceline 20 (* 23: ifeq[153](3) -> aload_0 *) goto branch2, branch3 branch2: assume topBool(st) = false st := pop(st) goto stmt61 branch3: assume !topBool(st) = false st := pop(st) stmt26: sourceline 22 (* 26: aload_0[42](1) *) st := push(st, _this) stmt27: sourceline 22 (* 27: getfield[180](3) 3 *) assert !topRef(st) = null ; "non-null field access receiver" st := push(pop(st), sel(h, topRef(st), field_Zune_days)) stmt30: sourceline 22 (* 30: sipush[17](3) 366 *) st := push(st, 366) stmt33: sourceline 22 (* 33: if_icmple[164](3) -> aload_0 *) goto branch4, branch5 branch4: assume top2Int(st) <= topInt(st) st := pop2(st) goto stmt0 branch5: assume !top2Int(st) <= topInt(st) st := pop2(st) stmt36: sourceline 24 (* 36: aload_0[42](1) *) st := push(st, _this) stmt37: sourceline 24 (* 37: dup[89](1) *) st := push(st, topRef(st)) stmt38: sourceline 24 (* 38: getfield[180](3) 3 *) assert !topRef(st) = null ; "non-null field access receiver" st := push(pop(st), sel(h, topRef(st), field_Zune_days)) stmt41: sourceline 24 (* 41: sipush[17](3) 366 *) st := push(st, 366) stmt44: sourceline 24 (* 44: isub[100](1) *) st := push(pop2(st), top2Int(st) - topInt(st)) stmt45: sourceline 24 (* 45: putfield[181](3) 3 *) assert !top2Ref(st) = null ; "non-null field access receiver" h := stor(h, top2Ref(st), field_Zune_days, topInt(st)) st := pop2(st) stmt48: sourceline 25 (* 48: aload_0[42](1) *) st := push(st, _this) stmt49: sourceline 25 (* 49: dup[89](1) *) st := push(st, topRef(st)) stmt50: sourceline 25 (* 50: getfield[180](3) 2 *) assert !topRef(st) = null ; "non-null field access receiver" st := push(pop(st), sel(h, topRef(st), field_Zune_year)) stmt53: sourceline 25 (* 53: iconst_1[4](1) *) st := push(st, 1) stmt54: sourceline 25 (* 54: iadd[96](1) *) st := push(pop2(st), topInt(st) + top2Int(st)) stmt55: sourceline 25 (* 55: putfield[181](3) 2 *) assert !top2Ref(st) = null ; "non-null field access receiver" h := stor(h, top2Ref(st), field_Zune_year, topInt(st)) st := pop2(st) stmt58: sourceline 25 (* 58: goto[167](3) -> aload_0 *) goto stmt0 stmt61: sourceline 30 (* 61: aload_0[42](1) *) st := push(st, _this) stmt62: sourceline 30 (* 62: dup[89](1) *) st := push(st, topRef(st)) stmt63: sourceline 30 (* 63: getfield[180](3) 3 *) assert !topRef(st) = null ; "non-null field access receiver" st := push(pop(st), sel(h, topRef(st), field_Zune_days)) stmt66: sourceline 30 (* 66: sipush[17](3) 365 *) st := push(st, 365) stmt69: sourceline 30 (* 69: isub[100](1) *) st := push(pop2(st), top2Int(st) - topInt(st)) stmt70: sourceline 30 (* 70: putfield[181](3) 3 *) assert !top2Ref(st) = null ; "non-null field access receiver" h := stor(h, top2Ref(st), field_Zune_days, topInt(st)) st := pop2(st) stmt73: sourceline 31 (* 73: aload_0[42](1) *) st := push(st, _this) stmt74: sourceline 31 (* 74: dup[89](1) *) st := push(st, topRef(st)) stmt75: sourceline 31 (* 75: getfield[180](3) 2 *) assert !topRef(st) = null ; "non-null field access receiver" st := push(pop(st), sel(h, topRef(st), field_Zune_year)) stmt78: sourceline 31 (* 78: iconst_1[4](1) *) st := push(st, 1) stmt79: sourceline 31 (* 79: iadd[96](1) *) st := push(pop2(st), topInt(st) + top2Int(st)) stmt80: sourceline 31 (* 80: putfield[181](3) 2 *) assert !top2Ref(st) = null ; "non-null field access receiver" h := stor(h, top2Ref(st), field_Zune_year, topInt(st)) st := pop2(st) stmt83: sourceline 31 (* 83: goto[167](3) -> aload_0 *) goto stmt0 stmt86: sourceline 35 (* 86: return[177](1) *) exc := null goto end_of_proc end_of_proc: assert sel(h, _this, field_Zune_days) >= 0 assert sel(h, _this, field_Zune_year) >= 1980 assert sel(h, _this, field_Zune_days) <= 365 assert true ; "Missing : Modifies PO ;(" (* end of program *) problem [[0 ; P]]