(* created : Thu Nov 19 18:45:10 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 *) function bool leap(int) (* Program declarations *) function (* local variables *) ref _this assignable field(int) field_GoodZune_year unique field(int) field_GoodZune_days unique (* Program *) program P source "GoodZune.java" assume sel(h, _this, field_GoodZune_days) >= 0 assume sel(h, _this, field_GoodZune_year) >= 1980 assume !_this = null & sel(h, _this, created) assume true stmt0: sourceline 23 (* 0: ldc[18](2) 3 *) skip_loopinv (* invariant *) sel(h, _this, field_GoodZune_days) >= 0 & sel(h, _this, field_GoodZune_year) >= 1980, (* variant *) sel(h, _this, field_GoodZune_days) stmt5: sourceline 27 (* 5: aload_0[42](1) *) st := push(st, _this) stmt6: sourceline 27 (* 6: aload_0[42](1) *) st := push(st, _this) stmt7: sourceline 27 (* 7: getfield[180](3) 2 *) assert !topRef(st) = null ; "non-null field access receiver" st := push(pop(st), sel(h, topRef(st), field_GoodZune_year)) stmt10: sourceline 27 (* 10: invokevirtual[182](3) 5 *) assert !top2Ref(st) = null ; "non-null method receiver" assert topInt(st) > 0 ; "establish pre condition" havoc anon h := disturb(h, anon, nothing) assume exc = null & boolRet = leap(topInt(st)) ; "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) stmt13: sourceline 27 (* 13: ifeq[153](3) -> aload_0 *) goto branch0, branch1 branch0: assume topInt(st) = 0 st := pop(st) goto stmt51 branch1: assume !topInt(st) = 0 st := pop(st) stmt16: sourceline 29 (* 16: aload_0[42](1) *) st := push(st, _this) stmt17: sourceline 29 (* 17: getfield[180](3) 6 *) assert !topRef(st) = null ; "non-null field access receiver" st := push(pop(st), sel(h, topRef(st), field_GoodZune_days)) stmt20: sourceline 29 (* 20: sipush[17](3) 366 *) st := push(st, 366) stmt23: sourceline 29 (* 23: if_icmple[164](3) -> return *) goto branch2, branch3 branch2: assume top2Int(st) <= topInt(st) st := pop2(st) goto stmt86 branch3: assume !top2Int(st) <= topInt(st) st := pop2(st) stmt26: sourceline 30 (* 26: aload_0[42](1) *) st := push(st, _this) stmt27: sourceline 30 (* 27: dup[89](1) *) st := push(st, topRef(st)) stmt28: sourceline 30 (* 28: getfield[180](3) 6 *) assert !topRef(st) = null ; "non-null field access receiver" st := push(pop(st), sel(h, topRef(st), field_GoodZune_days)) stmt31: sourceline 30 (* 31: sipush[17](3) 366 *) st := push(st, 366) stmt34: sourceline 30 (* 34: isub[100](1) *) st := push(pop2(st), top2Int(st) - topInt(st)) stmt35: sourceline 30 (* 35: putfield[181](3) 6 *) assert !top2Ref(st) = null ; "non-null field access receiver" h := stor(h, top2Ref(st), field_GoodZune_days, topInt(st)) st := pop2(st) stmt38: sourceline 31 (* 38: aload_0[42](1) *) st := push(st, _this) stmt39: sourceline 31 (* 39: dup[89](1) *) st := push(st, topRef(st)) stmt40: sourceline 31 (* 40: getfield[180](3) 2 *) assert !topRef(st) = null ; "non-null field access receiver" st := push(pop(st), sel(h, topRef(st), field_GoodZune_year)) stmt43: sourceline 31 (* 43: iconst_1[4](1) *) st := push(st, 1) stmt44: sourceline 31 (* 44: iadd[96](1) *) st := push(pop2(st), topInt(st) + top2Int(st)) stmt45: sourceline 31 (* 45: putfield[181](3) 2 *) assert !top2Ref(st) = null ; "non-null field access receiver" h := stor(h, top2Ref(st), field_GoodZune_year, topInt(st)) st := pop2(st) stmt48: sourceline 31 (* 48: goto[167](3) -> ldc 3 *) goto stmt0 stmt51: sourceline 38 (* 51: aload_0[42](1) *) st := push(st, _this) stmt52: sourceline 38 (* 52: getfield[180](3) 6 *) assert !topRef(st) = null ; "non-null field access receiver" st := push(pop(st), sel(h, topRef(st), field_GoodZune_days)) stmt55: sourceline 38 (* 55: sipush[17](3) 365 *) st := push(st, 365) stmt58: sourceline 38 (* 58: if_icmple[164](3) -> return *) goto branch4, branch5 branch4: assume top2Int(st) <= topInt(st) st := pop2(st) goto stmt86 branch5: assume !top2Int(st) <= topInt(st) st := pop2(st) stmt61: sourceline 39 (* 61: aload_0[42](1) *) st := push(st, _this) stmt62: sourceline 39 (* 62: dup[89](1) *) st := push(st, topRef(st)) stmt63: sourceline 39 (* 63: getfield[180](3) 6 *) assert !topRef(st) = null ; "non-null field access receiver" st := push(pop(st), sel(h, topRef(st), field_GoodZune_days)) stmt66: sourceline 39 (* 66: sipush[17](3) 365 *) st := push(st, 365) stmt69: sourceline 39 (* 69: isub[100](1) *) st := push(pop2(st), top2Int(st) - topInt(st)) stmt70: sourceline 39 (* 70: putfield[181](3) 6 *) assert !top2Ref(st) = null ; "non-null field access receiver" h := stor(h, top2Ref(st), field_GoodZune_days, topInt(st)) st := pop2(st) stmt73: sourceline 40 (* 73: aload_0[42](1) *) st := push(st, _this) stmt74: sourceline 40 (* 74: dup[89](1) *) st := push(st, topRef(st)) stmt75: sourceline 40 (* 75: getfield[180](3) 2 *) assert !topRef(st) = null ; "non-null field access receiver" st := push(pop(st), sel(h, topRef(st), field_GoodZune_year)) stmt78: sourceline 40 (* 78: iconst_1[4](1) *) st := push(st, 1) stmt79: sourceline 40 (* 79: iadd[96](1) *) st := push(pop2(st), topInt(st) + top2Int(st)) stmt80: sourceline 40 (* 80: putfield[181](3) 2 *) assert !top2Ref(st) = null ; "non-null field access receiver" h := stor(h, top2Ref(st), field_GoodZune_year, topInt(st)) st := pop2(st) stmt83: sourceline 40 (* 83: goto[167](3) -> ldc 3 *) goto stmt0 stmt86: sourceline 48 (* 86: return[177](1) *) exc := null goto end_of_proc end_of_proc: assert sel(h, _this, field_GoodZune_days) >= 0 assert sel(h, _this, field_GoodZune_year) >= 1980 assert sel(h, _this, field_GoodZune_days) <= 366 & sel(h, _this, field_GoodZune_days) = 366 -> leap(sel(h, _this, field_GoodZune_year)) (* end of program *) problem [[0 ; P]]