Messages

Last Msg First Msg

method | net.sourceforge.pebble.domain.Month__static_init

method | void net.sourceforge.pebble.domain.Month(Year, int)
pre | month >= -231+1
pre | year != null
pre | year.blog != null
pre | init'ed(year.year)
presumption | java.util.Calendar:getActualMaximum(...)@71 in 0..232-2
presumption | net.sourceforge.pebble.domain.Blog:getCalendar(... )@69 != null
post | this.blog == year.blog
post | this.blog != null
post | this.dailyBlogs == &new Day[](Month#1)
post | init'ed(this.date)
post | (soft) this.lastDayInMonth in 0..232-2
post | this.dailyBlogs.length == this.lastDayInMonth
post | this.month == month
post | this.month >= -231+1
post | this.year == year
post | this.year != null
post | (soft) new ArrayList(Day#1) num objects <= 232-2
post | (soft) new ArrayList(Day#2) num objects <= 232-2
post | (soft) new ArrayList(Day#3) num objects <= 232-2
post | (soft) new Day(Month#2) num objects <= 232-2
post | init'ed(new Day(Month#2).blog)
post | init'ed(new Day(Month#2).blogEntries)
post | init'ed(new Day(Month#2).date)
post | init'ed(new Day(Month#2).day)
post | init'ed(new Day(Month#2).month)
post | init'ed(new Day(Month#2).publishedBlogEntries)
post | init'ed(new Day(Month#2).unpublishedBlogEntries)
post | new Day[](Month#1) num objects == 1
post | init'ed(this.dailyBlogs[...])
post | (soft) new ArrayList(Day#1) num objects == java.util.Calendar:getActualMaximum(...)@71
post | (soft) new ArrayList(Day#2) num objects == java.util.Calendar:getActualMaximum(...)@71
post | (soft) new ArrayList(Day#3) num objects == java.util.Calendar:getActualMaximum(...)@71
post | (soft) new Day(Month#2) num objects == java.util.Calendar:getActualMaximum(...)@71
unanalyzed | call on getMonth
unanalyzed | call on getBlog
unanalyzed | call on net.sourceforge.pebble.domain. Blog:getCalendar
unanalyzed | call on java.util.Calendar:set
unanalyzed | call on java.util.Calendar:getTime
unanalyzed | call on net.sourceforge.pebble.domain. Month:getBlog
unanalyzed | call on getYear
unanalyzed | call on java.util.ArrayList
unanalyzed | call on net.sourceforge.pebble.domain.TimePeriod
unanalyzed | call on setDate

| info | method not available | -- call on Calendar net.sourceforge.pebble.domain. Blog:getCalendar()

method | Calendar getCalendar()
pre | this.blog != null
pre | this.month >= -231+1
pre | this.year != null
pre | init'ed(this.year.year)
presumption | net.sourceforge.pebble.domain.Blog:getCalendar(... )@84 != null
post | (soft) return_value != null

| info | method not available | -- call on Calendar net.sourceforge.pebble.domain. Blog:getCalendar()

method | Year getYear()
pre | init'ed(this.year)
post | return_value == this.year
post | init'ed(return_value)

method | int getMonth()
pre | init'ed(this.month)
post | return_value == this.month
post | init'ed(return_value)

method | String getPermalink()
pre | this.blog != null
post | return_value != null
pre | this.blog.permalinkProvider != null
pre | (soft) net/sourceforge/pebble/domain/BlogManager. instance != null
pre | (soft) init'ed(net/sourceforge/pebble/domain/BlogMa nager.instance.multiBlog)
pre | (soft) init'ed(this.blog.id)
test_vector | java.lang.String:length(...)@121: {0}, {1..232-1}
unanalyzed | call on java.lang.String:valueOf
unanalyzed | call on java.lang.String:indexOf
unanalyzed | call on net.sourceforge.pebble.PebbleContext:getIns tance
unanalyzed | call on net.sourceforge.pebble.PebbleContext:getCon figuration
unanalyzed | call on java.lang.String:length
unanalyzed | call on java.lang.String:substring
test_vector | getPermalink(...)@120: Addr_Set{null}, Inverse{null}

| info | method not available | -- call on String getPermalink(Month)

method | bool hasBlogEntries()
pre | (soft) this.dailyBlogs != null
pre | (soft) this.dailyBlogs.length >= 1
pre | (soft) this.dailyBlogs[...] != null
pre | (soft) this.dailyBlogs[...]. publishedBlogEntries != null
pre | (soft) this.lastDayInMonth <= 232-2
post | init'ed(return_value)
unanalyzed | call on java.lang.IllegalArgumentException
unanalyzed | call on java.util.List:isEmpty

Prev Msg Next Msg

| low
| precondition failure | net/sourceforge/pebble/domain/Month.getBlogForDay: day <= this.dailyBlogs.length

Prev Msg Next Msg

method | List getBlogEntries()
pre | this.dailyBlogs != null
pre | this.dailyBlogs.length <= 232-1
pre | this.lastDayInMonth - this.dailyBlogs.length in -231..232-1
pre | (soft) init'ed(this.dailyBlogs[...])
pre | (soft) init'ed(this.dailyBlogs[...]. blogEntries)
pre | (soft) init'ed(this.lastDayInMonth)
post | return_value == &new ArrayList(getBlogEntries#1 )
post | new ArrayList(getBlogEntries#1) num objects == 1
unanalyzed | call on java.lang.IllegalArgumentException
unanalyzed | call on java.util.ArrayList

Prev Msg Next Msg

| medium
| null dereference | check might fail: requires day != null

Prev Msg Next Msg

method | int getNumberOfBlogEntries()
pre | this.dailyBlogs != null
pre | this.dailyBlogs.length <= 232-1
pre | this.lastDayInMonth - this.dailyBlogs.length in -231..232-1
pre | (soft) init'ed(this.dailyBlogs[...])
pre | (soft) this.dailyBlogs[...]. publishedBlogEntries != null
pre | (soft) init'ed(this.lastDayInMonth)
post | init'ed(return_value)
unanalyzed | call on java.lang.IllegalArgumentException
unanalyzed | call on java.util.List:size

Prev Msg Next Msg

| medium
| null dereference | check might fail: requires day != null

Prev Msg Next Msg

method | Day[] getAllDays()
pre | this.dailyBlogs != null
pre | this.dailyBlogs.length <= 232-1
pre | this.lastDayInMonth - this.dailyBlogs.length in -231..232-1
pre | (soft) init'ed(this.dailyBlogs[...])
pre | (soft) init'ed(this.lastDayInMonth)
post | return_value == &new Day[](getAllDays#1)
post | new Day[](getAllDays#1) num objects == 1
post | return_value.length == this.dailyBlogs.length
post | return_value.length <= 232-1
post | possibly_updated(return_value[...])
post | this.lastDayInMonth - this.dailyBlogs.length in -231..232-1
unanalyzed | call on java.lang.IllegalArgumentException

Prev Msg Next Msg

| low
| precondition failure | net/sourceforge/pebble/domain/Month.getBlogForDay: this.lastDayInMonth >= 1
| low
| precondition failure | net/sourceforge/pebble/domain/Month.getBlogForDay: this.lastDayInMonth - day in 0..232-2

Prev Msg Next Msg

method | Day getBlogForDay(int)
pre | day >= 1
pre | this.dailyBlogs != null
pre | this.dailyBlogs.length >= 1
pre | day <= this.dailyBlogs.length
pre | this.lastDayInMonth >= 1
pre | this.lastDayInMonth - day in 0..232-2
pre | (soft) init'ed(this.dailyBlogs[...])
post | return_value == this.dailyBlogs[...]
post | init'ed(return_value)

method | Day getBlogForFirstDay()
pre | this.dailyBlogs != null
pre | this.dailyBlogs.length >= 1
pre | this.lastDayInMonth >= 1
pre | (soft) init'ed(this.dailyBlogs[...])
post | return_value == this.dailyBlogs[...]
post | init'ed(return_value)
unanalyzed | call on java.lang.IllegalArgumentException

method | Day getBlogForLastDay()
pre | this.dailyBlogs != null
pre | this.dailyBlogs.length >= 1
pre | this.lastDayInMonth <= this.dailyBlogs.length
pre | this.lastDayInMonth >= 1
pre | (soft) init'ed(this.dailyBlogs[...])
post | return_value == this.dailyBlogs[...]
post | init'ed(return_value)
unanalyzed | call on java.lang.IllegalArgumentException

method | int getLastDayInMonth()
pre | init'ed(this.lastDayInMonth)
post | return_value == this.lastDayInMonth
post | init'ed(return_value)

method | Month getPreviousMonth()
pre | this.month <= 13
pre | this.year != null
pre | (soft) this.month <= this.year.months.length + 1
pre | (soft) this.year.blog != null
pre | (soft) this.year.months != null
pre | (soft) init'ed(this.year.months[...])
post | init'ed(return_value)
unanalyzed | call on java.lang.IllegalArgumentException
unanalyzed | call on getMonth
unanalyzed | call on getBlog
unanalyzed | call on getBlogForPreviousYear
pre | (soft) this.year.blog.years != null
pre | (soft) this.year.year >= -231+1
post | init'ed(new ArrayList(Day#1) num objects)
post | init'ed(new ArrayList(Day#2) num objects)
post | init'ed(new ArrayList(Day#3) num objects)
post | init'ed(new Day(Month#2) num objects)
post | init'ed(new Day(Month#2).blog)
post | init'ed(new Day(Month#2).blogEntries)
post | init'ed(new Day(Month#2).date)
post | init'ed(new Day(Month#2).day)
post | init'ed(new Day(Month#2).month)
post | init'ed(new Day(Month#2).publishedBlogEntries)
post | init'ed(new Day(Month#2).unpublishedBlogEntries)
post | new Day[](Month#1) num objects in {0, 12}
post | init'ed(new Day[](Month#1).length)
post | init'ed(new Day[](Month#1)[...])
post | new Month(init#2) num objects in {0, 12}
post | new Month(init#2).blog != null
post | new Month(init#2).dailyBlogs != null
post | init'ed(new Month(init#2).date)
post | init'ed(new Month(init#2).lastDayInMonth)
post | new Month(init#2).month == 13
post | new Month(init#2).year != null
unanalyzed | call on net.sourceforge.pebble.domain. Blog:getCalendar
unanalyzed | call on java.util.Calendar:set
unanalyzed | call on java.util.Calendar:getTime
unanalyzed | call on java.util.Calendar:setTime
unanalyzed | call on java.util.Calendar:getActualMaximum
unanalyzed | call on getYear
unanalyzed | call on net.sourceforge.pebble.domain. Month:getBlog
unanalyzed | call on net.sourceforge.pebble.domain.TimePeriod
unanalyzed | call on java.util.ArrayList
unanalyzed | call on setDate
unanalyzed | call on net.sourceforge.pebble.domain.Month
unanalyzed | call on java.util.List:iterator
unanalyzed | call on java.util.List:add
unanalyzed | call on java.util.Collections:sort

method | Month getNextMonth()
pre | this.month >= 0
pre | this.year != null
pre | (soft) this.month - this.year.months.length in {-Inf..-1, 12..232-1}
pre | (soft) this.year.blog != null
pre | (soft) this.year.months != null
pre | (soft) init'ed(this.year.months[...])
post | init'ed(return_value)
unanalyzed | call on java.lang.IllegalArgumentException
unanalyzed | call on getMonth
unanalyzed | call on getBlog
unanalyzed | call on getBlogForNextYear
pre | (soft) this.year.blog.years != null
pre | (soft) this.year.year <= 232-2
post | init'ed(new ArrayList(Day#1) num objects)
post | init'ed(new ArrayList(Day#2) num objects)
post | init'ed(new ArrayList(Day#3) num objects)
post | init'ed(new Day(Month#2) num objects)
post | init'ed(new Day(Month#2).blog)
post | init'ed(new Day(Month#2).blogEntries)
post | init'ed(new Day(Month#2).date)
post | init'ed(new Day(Month#2).day)
post | init'ed(new Day(Month#2).month)
post | init'ed(new Day(Month#2).publishedBlogEntries)
post | init'ed(new Day(Month#2).unpublishedBlogEntries)
post | new Day[](Month#1) num objects in {0, 12}
post | init'ed(new Day[](Month#1).length)
post | init'ed(new Day[](Month#1)[...])
post | new Month(init#2) num objects in {0, 12}
post | new Month(init#2).blog != null
post | new Month(init#2).dailyBlogs != null
post | init'ed(new Month(init#2).date)
post | init'ed(new Month(init#2).lastDayInMonth)
post | new Month(init#2).month == 13
post | new Month(init#2).year != null
unanalyzed | call on net.sourceforge.pebble.domain. Blog:getCalendar
unanalyzed | call on java.util.Calendar:set
unanalyzed | call on java.util.Calendar:getTime
unanalyzed | call on java.util.Calendar:setTime
unanalyzed | call on java.util.Calendar:getActualMaximum
unanalyzed | call on getYear
unanalyzed | call on net.sourceforge.pebble.domain. Month:getBlog
unanalyzed | call on net.sourceforge.pebble.domain.TimePeriod
unanalyzed | call on java.util.ArrayList
unanalyzed | call on setDate
unanalyzed | call on net.sourceforge.pebble.domain.Month
unanalyzed | call on java.util.List:iterator
unanalyzed | call on java.util.List:add
unanalyzed | call on java.util.Collections:sort

method | bool before(Month)
pre | month != null
pre | init'ed(month.date)
pre | this.date != null
post | init'ed(return_value)

method | bool after(Month)
pre | month != null
pre | init'ed(month.date)
pre | this.date != null
post | init'ed(return_value)

method | Day getBlogForPreviousDay(Day)
pre | day != null
pre | init'ed(day.day)
pre | (soft) day.day <= this.dailyBlogs.length + 1
pre | (soft) this.dailyBlogs != null
pre | (soft) this.dailyBlogs.length >= 1
pre | (soft) init'ed(this.dailyBlogs[...])
pre | (soft) init'ed(this.lastDayInMonth)
pre | (soft) this.year != null
pre | (soft) this.year.blog != null
pre | (soft) this.year.months != null
post | init'ed(return_value)
unanalyzed | call on java.lang.IllegalArgumentException
unanalyzed | call on getMonth
unanalyzed | call on getBlog
unanalyzed | call on getBlogForPreviousYear
test_vector | day.day: {-231..1}, {2..232-1}
pre | (soft) this.month <= 13
pre | (soft) this.month <= this.year.months.length + 1
pre | (soft) this.year.blog.years != null
pre | (soft) init'ed(this.year.months[...])
pre | (soft) this.year.year >= -231+1
presumption | getBlogForPreviousMonth(...).dailyBlogs.length@281 >= 1
presumption | getBlogForPreviousMonth(...).dailyBlogs@281 != null
presumption | getBlogForPreviousMonth(...).lastDayInMonth@281 >= 1
post | init'ed(new ArrayList(Day#1) num objects)
post | init'ed(new ArrayList(Day#2) num objects)
post | init'ed(new ArrayList(Day#3) num objects)
post | init'ed(new Day(Month#2) num objects)
post | init'ed(new Day(Month#2).blog)
post | init'ed(new Day(Month#2).blogEntries)
post | init'ed(new Day(Month#2).date)
post | init'ed(new Day(Month#2).day)
post | init'ed(new Day(Month#2).month)
post | init'ed(new Day(Month#2).publishedBlogEntries)
post | init'ed(new Day(Month#2).unpublishedBlogEntries)
unanalyzed | call on net.sourceforge.pebble.domain. Blog:getCalendar
unanalyzed | call on java.util.Calendar:set
unanalyzed | call on java.util.Calendar:getTime
unanalyzed | call on java.util.Calendar:setTime
unanalyzed | call on java.util.Calendar:getActualMaximum
unanalyzed | call on getYear
unanalyzed | call on net.sourceforge.pebble.domain. Month:getBlog
unanalyzed | call on net.sourceforge.pebble.domain.TimePeriod
unanalyzed | call on java.util.ArrayList
unanalyzed | call on setDate
unanalyzed | call on net.sourceforge.pebble.domain.Month
unanalyzed | call on java.util.List:iterator
unanalyzed | call on java.util.List:add
unanalyzed | call on java.util.Collections:sort

Prev Msg Next Msg

| low
| precondition failure | net/sourceforge/pebble/domain/Month.getBlogForDay: this.lastDayInMonth >= 1
+ |
| low
| precondition failure | net/sourceforge/pebble/domain/Month.getBlogForDay: this.lastDayInMonth - day in 0..232-2

Prev Msg Next Msg

Prev Msg Next Msg

+ |
| medium
| null dereference | check might fail: requires getBlogForPreviousMonth( ...) != null
| low
| precondition failure | net/sourceforge/pebble/domain/Month. getBlogForLastDay: this.lastDayInMonth <= this.dailyBlogs.length
+ |
| low
| precondition failure | net/sourceforge/pebble/domain/Month. getBlogForLastDay: this.dailyBlogs.length >= 1
+ |
| low
| precondition failure | net/sourceforge/pebble/domain/Month. getBlogForLastDay: this.lastDayInMonth >= 1

Prev Msg Next Msg

method | Day getBlogForNextDay(Day)
pre | day != null
pre | init'ed(day.day)
pre | day.day - this.lastDayInMonth in -232+1.. 6_442_450_943
pre | init'ed(this.lastDayInMonth)
pre | (soft) day.day < this.dailyBlogs.length
pre | (soft) this.dailyBlogs != null
pre | (soft) this.dailyBlogs.length >= 1
pre | (soft) init'ed(this.dailyBlogs[...])
pre | (soft) this.month - this.year.months.length in {-Inf..-1, 12..232-1}
pre | (soft) this.year != null
pre | (soft) this.year.blog != null
pre | (soft) this.year.months != null
post | init'ed(return_value)
unanalyzed | call on java.lang.IllegalArgumentException
unanalyzed | call on getMonth
unanalyzed | call on getBlog
unanalyzed | call on getBlogForNextYear
test_vector | day.day - this.lastDayInMonth: {0..6_442_450_943}, {-232+1..-1}
pre | (soft) this.month >= 0
pre | (soft) this.year.blog.years != null
pre | (soft) init'ed(this.year.months[...])
pre | (soft) this.year.year <= 232-2
presumption | getBlogForNextMonth(...).dailyBlogs.length@296 >= 1
presumption | getBlogForNextMonth(...).dailyBlogs@296 != null
presumption | getBlogForNextMonth(...).lastDayInMonth@296 >= 1
post | init'ed(new ArrayList(Day#1) num objects)
post | init'ed(new ArrayList(Day#2) num objects)
post | init'ed(new ArrayList(Day#3) num objects)
post | init'ed(new Day(Month#2) num objects)
post | init'ed(new Day(Month#2).blog)
post | init'ed(new Day(Month#2).blogEntries)
post | init'ed(new Day(Month#2).date)
post | init'ed(new Day(Month#2).day)
post | init'ed(new Day(Month#2).month)
post | init'ed(new Day(Month#2).publishedBlogEntries)
post | init'ed(new Day(Month#2).unpublishedBlogEntries)
unanalyzed | call on net.sourceforge.pebble.domain. Blog:getCalendar
unanalyzed | call on java.util.Calendar:set
unanalyzed | call on java.util.Calendar:getTime
unanalyzed | call on java.util.Calendar:setTime
unanalyzed | call on java.util.Calendar:getActualMaximum
unanalyzed | call on getYear
unanalyzed | call on net.sourceforge.pebble.domain. Month:getBlog
unanalyzed | call on net.sourceforge.pebble.domain.TimePeriod
unanalyzed | call on java.util.ArrayList
unanalyzed | call on setDate
unanalyzed | call on net.sourceforge.pebble.domain.Month
unanalyzed | call on java.util.List:iterator
unanalyzed | call on java.util.List:add
unanalyzed | call on java.util.Collections:sort

Prev Msg Next Msg

| low
| precondition failure | net/sourceforge/pebble/domain/Month.getBlogForDay: day >= 1

Prev Msg Next Msg

Prev Msg Next Msg

+ |
| medium
| null dereference | check might fail: requires getBlogForNextMonth(... ) != null
+ |
| low
| precondition failure | net/sourceforge/pebble/domain/Month. getBlogForFirstDay: this.dailyBlogs.length >= 1
+ |
| low
| precondition failure | net/sourceforge/pebble/domain/Month. getBlogForFirstDay: this.lastDayInMonth >= 1

Prev Msg Next Msg

method | String toString()
pre | init'ed(this.date)
post | init'ed(return_value)