Messages

Last Msg First Msg

method

net.sourceforge.pebble.domain.Month__static_init

method	void net.sourceforge.pebble.domain.Month(Year, int)
pre	month >= -2³¹+1
pre	year != null
pre	year.blog != null
pre	init'ed(year.year)
presumption	java.util.Calendar:getActualMaximum(...)@71 in 0..2³²-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..2³²-2
post	this.dailyBlogs.length == this.lastDayInMonth
post	this.month == month
post	this.month >= -2³¹+1
post	this.year == year
post	this.year != null
post	(soft) new ArrayList(Day#1) num objects <= 2³²-2
post	(soft) new ArrayList(Day#2) num objects <= 2³²-2
post	(soft) new ArrayList(Day#3) num objects <= 2³²-2
post	(soft) new Day(Month#2) num objects <= 2³²-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 >= -2³¹+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..2³²-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 <= 2³²-2
post	init'ed(return_value)
unanalyzed	call on java.lang.IllegalArgumentException
unanalyzed	call on java.util.List:isEmpty

Prev Msg Next Msg

click for all messages in this file 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 <= 2³²-1
pre	this.lastDayInMonth - this.dailyBlogs.length in -2³¹..2³²-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

click for all messages in this file medium

null dereference check might fail: requires day != null

Prev Msg Next Msg

method	int getNumberOfBlogEntries()
pre	this.dailyBlogs != null
pre	this.dailyBlogs.length <= 2³²-1
pre	this.lastDayInMonth - this.dailyBlogs.length in -2³¹..2³²-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

click for all messages in this file medium

null dereference check might fail: requires day != null

Prev Msg Next Msg

method	Day[] getAllDays()
pre	this.dailyBlogs != null
pre	this.dailyBlogs.length <= 2³²-1
pre	this.lastDayInMonth - this.dailyBlogs.length in -2³¹..2³²-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 <= 2³²-1
post	possibly_updated(return_value[...])
post	this.lastDayInMonth - this.dailyBlogs.length in -2³¹..2³²-1
unanalyzed	call on java.lang.IllegalArgumentException

Prev Msg Next Msg

click for all messages in this file 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..2³²-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..2³²-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 >= -2³¹+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..2³²-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 <= 2³²-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: {-2³¹..1}, {2..2³²-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 >= -2³¹+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

click for all messages in this file 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..2³²-2

Prev Msg Next Msg

Prev Msg Next Msg

+

click for all messages in this file medium

null dereference check might fail: requires getBlogForPreviousMonth( ...) != null

low

precondition failure net/sourceforge/pebble/domain/Month. getBlogForLastDay: this.lastDayInMonth <= this.dailyBlogs.length

+

click for all messages in this file 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 -2³²+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..2³²-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}, {-2³²+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 <= 2³²-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

click for all messages in this file low

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

Prev Msg Next Msg

Prev Msg Next Msg

+

click for all messages in this file medium

null dereference check might fail: requires getBlogForNextMonth(... ) != null

+

low

precondition failure net/sourceforge/pebble/domain/Month. getBlogForFirstDay: this.dailyBlogs.length >= 1

+

click for all messages in this file 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)