| method | void paintComponent(Graphics) |
| pre | graphics != null |
| pre | this.document != null |
| pre | this.document.lines != null |
| pre | this.positions != null |
| pre | init'ed(this.scrollBarPosition) |
| pre | this.textLayouts != null |
| pre | this.textPane != null |
| pre | (soft) this.document.cachedLines != null |
| pre | (soft) this.document.cachedStrings != null |
| pre | (soft) this.lineWrap != null |
| pre | (soft) this.selection != null |
| pre | (soft) init'ed(this.selection.endLine) |
| pre | (soft) init'ed(this.selection.endPos) |
| pre | (soft) init'ed(this.selection.startLine) |
| pre | (soft) init'ed(this.selection.startPos) |
| presumption | (int) ((float) (com.dmdirc.addons.ui_swing. textpane.TextPaneCanvas:getWidth(...)@122 - 6)) in {-2_147_483_654..4_294_967_289} |
| presumption | (int) ((float) (getLine(...).lineHeight)*21_617_278 _211_378_381/18_014_398_509_481_984) in {-231..232-1} |
| presumption | java.awt.Toolkit:getDefaultToolkit(...)@116 != null |
| presumption | java.awt.font.LineBreakMeasurer:nextLayout(... )@191 != null |
| presumption | java.text.AttributedString:getIterator(...)@253 != null |
| presumption | java.util.List:size(...)@78 >= -231+1 |
| presumption | java.util.Map:get(...)@174 != null |
| post | possibly_updated(this.firstVisibleLine) |
| post | possibly_updated(this.lastVisibleLine) |
| unanalyzed | call on java.awt.font.LineBreakMeasurer:getPosition |
| unanalyzed | call on java.awt.font.LineBreakMeasurer:nextLayout |
| unanalyzed | call on java.awt.font.LineBreakMeasurer:setPosition |
| unanalyzed | call on java.lang.String:length |
| unanalyzed | call on java.util.Map:entrySet |
| unanalyzed | call on java.util.Set:iterator |
| unanalyzed | call on java.util.Map$Entry:getValue |
| unanalyzed | call on java.util.Map:get |
| unanalyzed | call on java.awt.font.TextLayout:getCharacterCount |
| unanalyzed | call on java.awt.font.TextLayout:hitTestChar |
| unanalyzed | call on java.awt.font.TextHitInfo:getInsertionIndex |
| unanalyzed | call on java.util.Map$Entry:getKey |
| unanalyzed | call on java.awt.Rectangle:contains |
| unanalyzed | call on java.awt.Point:getX |
| unanalyzed | call on java.awt.Point:getY |
| unanalyzed | call on getStyledLine |
| unanalyzed | call on java.text.AttributedCharacterIterator:setIn dex |
| unanalyzed | call on java.text.AttributedCharacterIterator:getAt tributes |
| unanalyzed | call on java.lang.String:instanceof |
| unanalyzed | call on java.text.AttributedCharacterIterator:getBe ginIndex |
| unanalyzed | call on java.text.AttributedCharacterIterator:getEn dIndex |
| unanalyzed | call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:getMousePosition |
| unanalyzed | call on getLine |
| unanalyzed | call on com.dmdirc.ui.messages.Styliser:stipControl Codes |
| unanalyzed | call on java.awt.Rectangle:getX |
| unanalyzed | call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:setCursor |
| unanalyzed | call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:getCursor |
| unanalyzed | call on java.awt.Cursor:getDefaultCursor |
| unanalyzed | call on java.lang.String:substring |
| unanalyzed | call on java.lang.String:isEmpty |
| unanalyzed | call on getLineHeight |
| unanalyzed | call on java.text.AttributedString |
| unanalyzed | call on com.dmdirc.addons.ui_swing.textpane. TextPane:getBackground |
| unanalyzed | call on java.text.AttributedString:addAttribute |
| unanalyzed | call on com.dmdirc.addons.ui_swing.textpane. TextPane:getForeground |
| unanalyzed | call on java.text.AttributedString:getIterator |
| unanalyzed | call on java.awt.Graphics2D:getFontRenderContext |
| unanalyzed | call on java.awt.font.TextLayout |
| unanalyzed | call on java.awt.font.TextLayout:getLogicalHighligh tShape |
| unanalyzed | call on java.awt.Shape:getBounds |
| unanalyzed | call on java.awt.Graphics2D:translate |
| unanalyzed | call on java.awt.font.TextLayout:draw |
| unanalyzed | call on java.util.List:get |
| unanalyzed | call on javax.swing.UIManager:getFont |
| unanalyzed | call on java.awt.Font:getSize |
| unanalyzed | call on com.dmdirc.util.RollingList:contains |
| unanalyzed | call on com.dmdirc.util.RollingList:getList |
| unanalyzed | call on java.util.List:indexOf |
| unanalyzed | call on com.dmdirc.util.RollingList:get |
| unanalyzed | call on com.dmdirc.ui.messages.Styliser:getStyledSt ring |
| unanalyzed | call on javax.swing.text.StyledDocument:getParagrap hElement |
| unanalyzed | call on javax.swing.text.Element:getDocument |
| unanalyzed | call on javax.swing.text.Document:getLength |
| unanalyzed | call on javax.swing.text.Document:getText |
| unanalyzed | call on java.lang.Throwable:__curr_excep_obj |
| unanalyzed | call on javax.swing.text.BadLocationException:getMe ssage |
| unanalyzed | call on com.dmdirc.logger.Logger:userError |
| unanalyzed | call on hasOption |
| unanalyzed | call on java.util.Map:containsKey |
| unanalyzed | call on java.lang.Integer:intValue |
| unanalyzed | call on java.lang.Integer:valueOf |
| unanalyzed | call on java.util.Map:put |
| unanalyzed | call on java.util.List:iterator |
| unanalyzed | call on getOption |
| unanalyzed | call on java.lang.IllegalArgumentException |
| unanalyzed | call on com.dmdirc.util.ConfigFile:getKeyDomain |
| unanalyzed | call on com.dmdirc.util.ConfigFile:isKeyDomain |
| unanalyzed | call on java.awt.Font:getName |
| unanalyzed | call on java.awt.Font |
| unanalyzed | call on java.awt.Font:getFamily |
| unanalyzed | call on javax.swing.text.Element:getElementCount |
| unanalyzed | call on javax.swing.text.Element:getElement |
| unanalyzed | call on javax.swing.text.Element:getAttributes |
| unanalyzed | call on javax.swing.text.AttributeSet:getAttributeN ames |
| unanalyzed | call on java.util.Enumeration:hasMoreElements |
| unanalyzed | call on java.util.Enumeration:nextElement |
| unanalyzed | call on javax.swing.text.AttributeSet:getAttribute |
| unanalyzed | call on javax.swing.text.Element:getStartOffset |
| unanalyzed | call on javax.swing.text.Element:getEndOffset |
| unanalyzed | call on com.dmdirc.util.RollingList:add |
| unanalyzed | call on java.util.List:size |
| test_vector | java.awt.Toolkit:getDesktopProperty(...)@116: Addr_Set{null}, Inverse{null} |
| test_vector | java.awt.font.TextLayout:isLeftToRight(...)@201: {0}, {1} |
| test_vector | java.util.List:size(...)@78: {0}, {-231.. -1, 1..232-1} |
| test_vector | java.util.Map:containsKey(...)@172: {0}, {1} |
| method | void doHighlight(int, int, TextLayout, Graphics2D, float, float) |
| pre | this.selection != null |
| pre | init'ed(this.selection.endLine) |
| pre | init'ed(this.selection.endPos) |
| pre | init'ed(this.selection.startLine) |
| pre | init'ed(this.selection.startPos) |
| pre | (soft) g != null |
| pre | (soft) layout != null |
| pre | (soft) this.document != null |
| pre | (soft) this.document.cachedLines != null |
| pre | (soft) this.document.cachedStrings != null |
| pre | (soft) this.document.lines != null |
| pre | (soft) this.textPane != null |
| presumption | (int) ((float) (getLine(...).lineHeight)*21_617_278 _211_378_381/18_014_398_509_481_984) in {-231..232-1} |
| presumption | (int) ((float) (getLineHeight(...)@333)*21_617_278_ 211_378_381/18_014_398_509_481_984) in range |
| presumption | (int) (drawPosY + (float) ((int) ((float) (getLine(...).lineHeight)*21_617_278_211_378_381/1 8_014_398_509_481_984))/2) in {-231.. 232-1} |
| presumption | (int) (drawPosY + (float) ((int) ((float) (getLineHeight(...)@333)*21_617_278_211_378_381/18 _014_398_509_481_984))/2) in range |
| presumption | chars + java.awt.font.TextLayout:getCharacterCount( ...)@314 in {-231..232-1} |
| presumption | com.dmdirc.ui.messages.Styliser:stipControlCodes(.. .)@107 != null |
| presumption | getLine(...).lineParts != null |
| presumption | getLine(...).lineParts.length <= 232-1 |
| presumption | java.awt.Shape:getBounds(...)@352 != null |
| presumption | java.awt.Shape:getBounds(...)@358 != null |
| presumption | init'ed(java.awt.font.TextAttribute.BACKGROUND) |
| presumption | init'ed(java.awt.font.TextAttribute.FOREGROUND) |
| presumption | java.awt.font.TextLayout:getLogicalHighlightShape(. ..)@346 != null |
| presumption | java.util.List:get(...)@89 != null |
| unanalyzed | call on com.dmdirc.ui.messages.Styliser:stipControl Codes |
| unanalyzed | call on java.util.List:get |
| unanalyzed | call on getStyledLine |
| unanalyzed | call on javax.swing.UIManager:getFont |
| unanalyzed | call on java.awt.Font:getSize |
| unanalyzed | call on com.dmdirc.util.RollingList:contains |
| unanalyzed | call on com.dmdirc.util.RollingList:getList |
| unanalyzed | call on java.util.List:indexOf |
| unanalyzed | call on com.dmdirc.util.RollingList:get |
| unanalyzed | call on com.dmdirc.ui.messages.Styliser:getStyledSt ring |
| unanalyzed | call on javax.swing.text.StyledDocument:getParagrap hElement |
| unanalyzed | call on javax.swing.text.Element:getDocument |
| unanalyzed | call on javax.swing.text.Document:getLength |
| unanalyzed | call on javax.swing.text.Document:getText |
| unanalyzed | call on java.text.AttributedString |
| unanalyzed | call on java.lang.Throwable:__curr_excep_obj |
| unanalyzed | call on javax.swing.text.BadLocationException:getMe ssage |
| unanalyzed | call on com.dmdirc.logger.Logger:userError |
| unanalyzed | call on hasOption |
| unanalyzed | call on java.util.Map:containsKey |
| unanalyzed | call on java.util.Map:get |
| unanalyzed | call on java.lang.Integer:intValue |
| unanalyzed | call on java.lang.Integer:valueOf |
| unanalyzed | call on java.util.Map:put |
| unanalyzed | call on java.util.List:iterator |
| unanalyzed | call on getOption |
| unanalyzed | call on java.lang.IllegalArgumentException |
| unanalyzed | call on java.lang.String:isEmpty |
| unanalyzed | call on com.dmdirc.util.ConfigFile:getKeyDomain |
| unanalyzed | call on com.dmdirc.util.ConfigFile:isKeyDomain |
| unanalyzed | call on java.awt.Font:getName |
| unanalyzed | call on java.text.AttributedString:getIterator |
| unanalyzed | call on java.text.AttributedCharacterIterator:getEn dIndex |
| unanalyzed | call on java.awt.Font |
| unanalyzed | call on java.text.AttributedString:addAttribute |
| unanalyzed | call on java.awt.Font:getFamily |
| unanalyzed | call on javax.swing.text.Element:getElementCount |
| unanalyzed | call on javax.swing.text.Element:getElement |
| unanalyzed | call on javax.swing.text.Element:getAttributes |
| unanalyzed | call on javax.swing.text.AttributeSet:getAttributeN ames |
| unanalyzed | call on java.util.Enumeration:hasMoreElements |
| unanalyzed | call on java.util.Enumeration:nextElement |
| unanalyzed | call on javax.swing.text.AttributeSet:getAttribute |
| unanalyzed | call on javax.swing.text.Element:getStartOffset |
| unanalyzed | call on javax.swing.text.Element:getEndOffset |
| unanalyzed | call on com.dmdirc.util.RollingList:add |
| unanalyzed | call on getLineHeight |
| test_vector | this.selection.endLine - this.selection.startLine: {1..6_442_450_943}, {-6_442_450_943..-1}, {0} |
| test_vector | this.selection.endPos - this.selection.startPos: {0..6_442_450_943}, {-6_442_450_943..-1} |
| test_vector | java.lang.String:isEmpty(...)@327: {0}, {1} |
| method | void mouseClicked(MouseEvent) |
| pre | e != null |
| pre | this.textPane != null |
| pre | (soft) this.document != null |
| pre | (soft) this.document.lines != null |
| pre | (soft) this.positions != null |
| pre | (soft) this.selection != null |
| pre | (soft) this.textLayouts != null |
| presumption | com.dmdirc.ui.messages.Styliser:stipControlCodes(.. .)@107 != null |
| presumption | extent.length@406 >= 2 |
| presumption | getLine(...).lineParts != null |
| presumption | getLine(...).lineParts.length <= 232-1 |
| presumption | getLine(...)@400 init'ed |
| presumption | java.util.List:get(...)@89 != null |
| post | possibly_updated(this.selection.endLine) |
| post | possibly_updated(this.selection.endPos) |
| post | possibly_updated(this.selection.startLine) |
| post | possibly_updated(this.selection.startPos) |
| unanalyzed | call on java.lang.String:length |
| unanalyzed | call on java.lang.String:charAt |
| unanalyzed | call on java.util.Map:entrySet |
| unanalyzed | call on java.util.Set:iterator |
| unanalyzed | call on java.util.Map$Entry:getValue |
| unanalyzed | call on java.util.Map:get |
| unanalyzed | call on java.awt.font.TextLayout:getCharacterCount |
| unanalyzed | call on java.awt.font.TextLayout:hitTestChar |
| unanalyzed | call on java.awt.font.TextHitInfo:getInsertionIndex |
| unanalyzed | call on java.util.Map$Entry:getKey |
| unanalyzed | call on java.awt.Rectangle:contains |
| unanalyzed | call on java.awt.Point:getX |
| unanalyzed | call on java.awt.Point:getY |
| unanalyzed | call on com.dmdirc.ui.messages.Styliser:stipControl Codes |
| unanalyzed | call on java.util.List:get |
| test_vector | java.awt.event.MouseEvent:getClickCount(...)@413: {-231..1, 3..232-1}, {2} |
| test_vector | java.awt.event.MouseEvent:getClickCount(...)@418: {-231..2, 4..232-1}, {3} |
| method | ClickType getClickType(LineInfo) |
| pre | lineInfo != null |
| pre | init'ed(lineInfo.line) |
| pre | (soft) init'ed(lineInfo.index) |
| pre | (soft) this.document != null |
| pre | (soft) this.document.cachedLines != null |
| pre | (soft) this.document.cachedStrings != null |
| pre | (soft) this.document.lines != null |
| presumption | init'ed(com.dmdirc.ui.messages.IRCTextAttribute. CHANNEL) |
| presumption | init'ed(com.dmdirc.ui.messages.IRCTextAttribute. HYPERLINK) |
| presumption | init'ed(com.dmdirc.ui.messages.IRCTextAttribute. NICKNAME) |
| presumption | getStyledLine(...)@439 init'ed |
| presumption | java.text.AttributedCharacterIterator:getAttributes (...)@444 != null |
| presumption | java.text.AttributedCharacterIterator:getAttributes (...)@449 != null |
| presumption | java.text.AttributedCharacterIterator:getAttributes (...)@454 != null |
| presumption | java.text.AttributedString:getIterator(...)@253 != null |
| post | return_value in Addr_Set{&com.dmdirc.addons.ui_ swing.textpane.ClickType__static_init.new ClickType(ClickType__static_init#3),&com. dmdirc.addons.ui_swing.textpane.ClickType__static_i nit.new ClickType(ClickType__static_init#2), &com.dmdir... |
| unanalyzed | call on java.util.List:get |
| unanalyzed | call on getStyledLine |
| unanalyzed | call on javax.swing.UIManager:getFont |
| unanalyzed | call on java.awt.Font:getSize |
| unanalyzed | call on com.dmdirc.util.RollingList:contains |
| unanalyzed | call on com.dmdirc.util.RollingList:getList |
| unanalyzed | call on java.util.List:indexOf |
| unanalyzed | call on com.dmdirc.util.RollingList:get |
| unanalyzed | call on com.dmdirc.ui.messages.Styliser:getStyledSt ring |
| unanalyzed | call on javax.swing.text.StyledDocument:getParagrap hElement |
| unanalyzed | call on javax.swing.text.Element:getDocument |
| unanalyzed | call on javax.swing.text.Document:getLength |
| unanalyzed | call on javax.swing.text.Document:getText |
| unanalyzed | call on java.text.AttributedString |
| unanalyzed | call on java.lang.Throwable:__curr_excep_obj |
| unanalyzed | call on javax.swing.text.BadLocationException:getMe ssage |
| unanalyzed | call on com.dmdirc.logger.Logger:userError |
| unanalyzed | call on hasOption |
| unanalyzed | call on java.util.Map:containsKey |
| unanalyzed | call on java.util.Map:get |
| unanalyzed | call on java.lang.Integer:intValue |
| unanalyzed | call on java.lang.Integer:valueOf |
| unanalyzed | call on java.util.Map:put |
| unanalyzed | call on java.util.List:iterator |
| unanalyzed | call on getOption |
| unanalyzed | call on java.lang.IllegalArgumentException |
| unanalyzed | call on java.lang.String:isEmpty |
| unanalyzed | call on com.dmdirc.util.ConfigFile:getKeyDomain |
| unanalyzed | call on com.dmdirc.util.ConfigFile:isKeyDomain |
| unanalyzed | call on java.awt.Font:getName |
| unanalyzed | call on java.text.AttributedString:getIterator |
| unanalyzed | call on java.text.AttributedCharacterIterator:getEn dIndex |
| unanalyzed | call on java.awt.Font |
| unanalyzed | call on java.text.AttributedString:addAttribute |
| unanalyzed | call on java.awt.Font:getFamily |
| unanalyzed | call on javax.swing.text.Element:getElementCount |
| unanalyzed | call on javax.swing.text.Element:getElement |
| unanalyzed | call on javax.swing.text.Element:getAttributes |
| unanalyzed | call on javax.swing.text.AttributeSet:getAttributeN ames |
| unanalyzed | call on java.util.Enumeration:hasMoreElements |
| unanalyzed | call on java.util.Enumeration:nextElement |
| unanalyzed | call on javax.swing.text.AttributeSet:getAttribute |
| unanalyzed | call on javax.swing.text.Element:getStartOffset |
| unanalyzed | call on javax.swing.text.Element:getEndOffset |
| unanalyzed | call on com.dmdirc.util.RollingList:add |
| test_vector | lineInfo.line: {-1}, {-231..-2, 0..232-1} |
| method | Object getAttributeValueAtPoint(LineInfo) |
| pre | lineInfo != null |
| pre | init'ed(lineInfo.line) |
| pre | (soft) init'ed(lineInfo.index) |
| pre | (soft) this.document != null |
| pre | (soft) this.document.cachedLines != null |
| pre | (soft) this.document.cachedStrings != null |
| pre | (soft) this.document.lines != null |
| presumption | init'ed(com.dmdirc.ui.messages.IRCTextAttribute. CHANNEL) |
| presumption | init'ed(com.dmdirc.ui.messages.IRCTextAttribute. HYPERLINK) |
| presumption | init'ed(com.dmdirc.ui.messages.IRCTextAttribute. NICKNAME) |
| presumption | getStyledLine(...)@475 init'ed |
| presumption | java.text.AttributedCharacterIterator:getAttributes (...)@478 != null |
| presumption | java.text.AttributedCharacterIterator:getAttributes (...)@483 != null |
| presumption | java.text.AttributedCharacterIterator:getAttributes (...)@487 != null |
| presumption | java.text.AttributedString:getIterator(...)@253 != null |
| post | init'ed(return_value) |
| unanalyzed | call on java.util.List:get |
| unanalyzed | call on getStyledLine |
| unanalyzed | call on javax.swing.UIManager:getFont |
| unanalyzed | call on java.awt.Font:getSize |
| unanalyzed | call on com.dmdirc.util.RollingList:contains |
| unanalyzed | call on com.dmdirc.util.RollingList:getList |
| unanalyzed | call on java.util.List:indexOf |
| unanalyzed | call on com.dmdirc.util.RollingList:get |
| unanalyzed | call on com.dmdirc.ui.messages.Styliser:getStyledSt ring |
| unanalyzed | call on javax.swing.text.StyledDocument:getParagrap hElement |
| unanalyzed | call on javax.swing.text.Element:getDocument |
| unanalyzed | call on javax.swing.text.Document:getLength |
| unanalyzed | call on javax.swing.text.Document:getText |
| unanalyzed | call on java.text.AttributedString |
| unanalyzed | call on java.lang.Throwable:__curr_excep_obj |
| unanalyzed | call on javax.swing.text.BadLocationException:getMe ssage |
| unanalyzed | call on com.dmdirc.logger.Logger:userError |
| unanalyzed | call on hasOption |
| unanalyzed | call on java.util.Map:containsKey |
| unanalyzed | call on java.util.Map:get |
| unanalyzed | call on java.lang.Integer:intValue |
| unanalyzed | call on java.lang.Integer:valueOf |
| unanalyzed | call on java.util.Map:put |
| unanalyzed | call on java.util.List:iterator |
| unanalyzed | call on getOption |
| unanalyzed | call on java.lang.IllegalArgumentException |
| unanalyzed | call on java.lang.String:isEmpty |
| unanalyzed | call on com.dmdirc.util.ConfigFile:getKeyDomain |
| unanalyzed | call on com.dmdirc.util.ConfigFile:isKeyDomain |
| unanalyzed | call on java.awt.Font:getName |
| unanalyzed | call on java.text.AttributedString:getIterator |
| unanalyzed | call on java.text.AttributedCharacterIterator:getEn dIndex |
| unanalyzed | call on java.awt.Font |
| unanalyzed | call on java.text.AttributedString:addAttribute |
| unanalyzed | call on java.awt.Font:getFamily |
| unanalyzed | call on javax.swing.text.Element:getElementCount |
| unanalyzed | call on javax.swing.text.Element:getElement |
| unanalyzed | call on javax.swing.text.Element:getAttributes |
| unanalyzed | call on javax.swing.text.AttributeSet:getAttributeN ames |
| unanalyzed | call on java.util.Enumeration:hasMoreElements |
| unanalyzed | call on java.util.Enumeration:nextElement |
| unanalyzed | call on javax.swing.text.AttributeSet:getAttribute |
| unanalyzed | call on javax.swing.text.Element:getStartOffset |
| unanalyzed | call on javax.swing.text.Element:getEndOffset |
| unanalyzed | call on com.dmdirc.util.RollingList:add |
| test_vector | lineInfo.line: {-1}, {-231..-2, 0..232-1} |
| method | void mousePressed(MouseEvent) |
| pre | e != null |
| pre | this.textPane != null |
| pre | (soft) this.positions != null |
| pre | (soft) this.selection != null |
| pre | (soft) this.textLayouts != null |
| post | possibly_updated(this.selection.endLine) |
| post | possibly_updated(this.selection.endPos) |
| post | possibly_updated(this.selection.startLine) |
| post | possibly_updated(this.selection.startPos) |
| unanalyzed | call on java.util.Map:entrySet |
| unanalyzed | call on java.util.Set:iterator |
| unanalyzed | call on java.util.Map$Entry:getValue |
| unanalyzed | call on java.util.Map:get |
| unanalyzed | call on java.awt.font.TextLayout:getCharacterCount |
| unanalyzed | call on java.awt.font.TextLayout:hitTestChar |
| unanalyzed | call on java.awt.font.TextHitInfo:getInsertionIndex |
| unanalyzed | call on java.util.Map$Entry:getKey |
| unanalyzed | call on java.awt.Rectangle:contains |
| unanalyzed | call on java.awt.Point:getX |
| unanalyzed | call on java.awt.Point:getY |
| unanalyzed | call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:repaint |
| unanalyzed | call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:isVisible |
| unanalyzed | call on java.awt.event.MouseEvent:getLocationOnScre en |
| unanalyzed | call on javax.swing.SwingUtilities:convertPointFrom Screen |
| unanalyzed | call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:contains |
| unanalyzed | call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:getBounds |
| unanalyzed | call on java.awt.event.MouseEvent:getPoint |
| unanalyzed | call on java.awt.Rectangle:getX |
| unanalyzed | call on java.awt.Point:setLocation |
| unanalyzed | call on java.awt.Rectangle:getWidth |
| unanalyzed | call on java.awt.Rectangle:getY |
| unanalyzed | call on java.awt.Rectangle:getHeight |
| test_vector | java.awt.event.MouseEvent:getButton(...)@567: {-231..0, 2..232-1}, {1} |
| method | void mouseReleased(MouseEvent) |
| pre | e != null |
| pre | this.textPane != null |
| pre | (soft) this.positions != null |
| pre | (soft) this.selection != null |
| pre | (soft) this.textLayouts != null |
| post | possibly_updated(this.selection.endLine) |
| post | possibly_updated(this.selection.endPos) |
| post | possibly_updated(this.selection.startLine) |
| post | possibly_updated(this.selection.startPos) |
| unanalyzed | call on java.util.Map:entrySet |
| unanalyzed | call on java.util.Set:iterator |
| unanalyzed | call on java.util.Map$Entry:getValue |
| unanalyzed | call on java.util.Map:get |
| unanalyzed | call on java.awt.font.TextLayout:getCharacterCount |
| unanalyzed | call on java.awt.font.TextLayout:hitTestChar |
| unanalyzed | call on java.awt.font.TextHitInfo:getInsertionIndex |
| unanalyzed | call on java.util.Map$Entry:getKey |
| unanalyzed | call on java.awt.Rectangle:contains |
| unanalyzed | call on java.awt.Point:getX |
| unanalyzed | call on java.awt.Point:getY |
| unanalyzed | call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:repaint |
| unanalyzed | call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:isVisible |
| unanalyzed | call on java.awt.event.MouseEvent:getLocationOnScre en |
| unanalyzed | call on javax.swing.SwingUtilities:convertPointFrom Screen |
| unanalyzed | call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:contains |
| unanalyzed | call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:getBounds |
| unanalyzed | call on java.awt.event.MouseEvent:getPoint |
| unanalyzed | call on java.awt.Rectangle:getX |
| unanalyzed | call on java.awt.Point:setLocation |
| unanalyzed | call on java.awt.Rectangle:getWidth |
| unanalyzed | call on java.awt.Rectangle:getY |
| unanalyzed | call on java.awt.Rectangle:getHeight |
| test_vector | java.awt.event.MouseEvent:getButton(...)@581: {-231..0, 2..232-1}, {1} |
| method | void mouseDragged(MouseEvent) |
| pre | e != null |
| pre | this.textPane != null |
| pre | (soft) this.positions != null |
| pre | (soft) this.selection != null |
| pre | (soft) this.textLayouts != null |
| post | possibly_updated(this.selection.endLine) |
| post | possibly_updated(this.selection.endPos) |
| post | possibly_updated(this.selection.startLine) |
| post | possibly_updated(this.selection.startPos) |
| unanalyzed | call on java.util.Map:entrySet |
| unanalyzed | call on java.util.Set:iterator |
| unanalyzed | call on java.util.Map$Entry:getValue |
| unanalyzed | call on java.util.Map:get |
| unanalyzed | call on java.awt.font.TextLayout:getCharacterCount |
| unanalyzed | call on java.awt.font.TextLayout:hitTestChar |
| unanalyzed | call on java.awt.font.TextHitInfo:getInsertionIndex |
| unanalyzed | call on java.util.Map$Entry:getKey |
| unanalyzed | call on java.awt.Rectangle:contains |
| unanalyzed | call on java.awt.Point:getX |
| unanalyzed | call on java.awt.Point:getY |
| unanalyzed | call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:repaint |
| unanalyzed | call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:isVisible |
| unanalyzed | call on java.awt.event.MouseEvent:getLocationOnScre en |
| unanalyzed | call on javax.swing.SwingUtilities:convertPointFrom Screen |
| unanalyzed | call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:contains |
| unanalyzed | call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:getBounds |
| unanalyzed | call on java.awt.event.MouseEvent:getPoint |
| unanalyzed | call on java.awt.Rectangle:getX |
| unanalyzed | call on java.awt.Point:setLocation |
| unanalyzed | call on java.awt.Rectangle:getWidth |
| unanalyzed | call on java.awt.Rectangle:getY |
| unanalyzed | call on java.awt.Rectangle:getHeight |
| test_vector | java.awt.event.MouseEvent:getModifiersEx(...)@595: {-231..1_023, 1_025..232-1}, {1_024} |
| method | void mouseMoved(MouseEvent) |
| pre | (soft) this.document != null |
| pre | (soft) this.document.cachedLines != null |
| pre | (soft) this.document.cachedStrings != null |
| pre | (soft) this.document.lines != null |
| pre | (soft) this.positions != null |
| pre | (soft) this.textLayouts != null |
| unanalyzed | call on java.util.Map:entrySet |
| unanalyzed | call on java.util.Set:iterator |
| unanalyzed | call on java.util.Map$Entry:getValue |
| unanalyzed | call on java.util.Map:get |
| unanalyzed | call on java.awt.font.TextLayout:getCharacterCount |
| unanalyzed | call on java.awt.font.TextLayout:hitTestChar |
| unanalyzed | call on java.awt.font.TextHitInfo:getInsertionIndex |
| unanalyzed | call on java.util.Map$Entry:getKey |
| unanalyzed | call on java.awt.Rectangle:contains |
| unanalyzed | call on java.awt.Point:getX |
| unanalyzed | call on java.awt.Point:getY |
| unanalyzed | call on getStyledLine |
| unanalyzed | call on java.text.AttributedCharacterIterator:setIn dex |
| unanalyzed | call on java.text.AttributedCharacterIterator:getAt tributes |
| unanalyzed | call on java.lang.String:instanceof |
| unanalyzed | call on java.text.AttributedCharacterIterator:getBe ginIndex |
| unanalyzed | call on java.text.AttributedCharacterIterator:getEn dIndex |
| unanalyzed | call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:getMousePosition |
| unanalyzed | call on getLine |
| unanalyzed | call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:setCursor |
| unanalyzed | call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:getCursor |
| unanalyzed | call on java.awt.Cursor:getDefaultCursor |
| unanalyzed | call on java.util.List:get |
| unanalyzed | call on javax.swing.UIManager:getFont |
| unanalyzed | call on java.awt.Font:getSize |
| unanalyzed | call on com.dmdirc.util.RollingList:contains |
| unanalyzed | call on com.dmdirc.util.RollingList:getList |
| unanalyzed | call on java.util.List:indexOf |
| unanalyzed | call on com.dmdirc.util.RollingList:get |
| unanalyzed | call on com.dmdirc.ui.messages.Styliser:getStyledSt ring |
| unanalyzed | call on javax.swing.text.StyledDocument:getParagrap hElement |
| unanalyzed | call on javax.swing.text.Element:getDocument |
| unanalyzed | call on javax.swing.text.Document:getLength |
| unanalyzed | call on javax.swing.text.Document:getText |
| unanalyzed | call on java.text.AttributedString |
| unanalyzed | call on java.lang.Throwable:__curr_excep_obj |
| unanalyzed | call on javax.swing.text.BadLocationException:getMe ssage |
| unanalyzed | call on com.dmdirc.logger.Logger:userError |
| unanalyzed | call on hasOption |
| unanalyzed | call on java.util.Map:containsKey |
| unanalyzed | call on java.lang.Integer:intValue |
| unanalyzed | call on java.lang.Integer:valueOf |
| unanalyzed | call on java.util.Map:put |
| unanalyzed | call on java.util.List:iterator |
| unanalyzed | call on getOption |
| unanalyzed | call on java.lang.IllegalArgumentException |
| unanalyzed | call on java.lang.String:isEmpty |
| unanalyzed | call on com.dmdirc.util.ConfigFile:getKeyDomain |
| unanalyzed | call on com.dmdirc.util.ConfigFile:isKeyDomain |
| unanalyzed | call on java.awt.Font:getName |
| unanalyzed | call on java.text.AttributedString:getIterator |
| unanalyzed | call on java.awt.Font |
| unanalyzed | call on java.text.AttributedString:addAttribute |
| unanalyzed | call on java.awt.Font:getFamily |
| unanalyzed | call on javax.swing.text.Element:getElementCount |
| unanalyzed | call on javax.swing.text.Element:getElement |
| unanalyzed | call on javax.swing.text.Element:getAttributes |
| unanalyzed | call on javax.swing.text.AttributeSet:getAttributeN ames |
| unanalyzed | call on java.util.Enumeration:hasMoreElements |
| unanalyzed | call on java.util.Enumeration:nextElement |
| unanalyzed | call on javax.swing.text.AttributeSet:getAttribute |
| unanalyzed | call on javax.swing.text.Element:getStartOffset |
| unanalyzed | call on javax.swing.text.Element:getEndOffset |
| unanalyzed | call on com.dmdirc.util.RollingList:add |
| method | void checkForLink() |
| pre | (soft) this.document != null |
| pre | (soft) this.document.cachedLines != null |
| pre | (soft) this.document.cachedStrings != null |
| pre | (soft) this.document.lines != null |
| pre | (soft) this.positions != null |
| pre | (soft) this.textLayouts != null |
| presumption | init'ed(com.dmdirc.ui.messages.IRCTextAttribute. CHANNEL) |
| presumption | init'ed(com.dmdirc.ui.messages.IRCTextAttribute. HYPERLINK) |
| presumption | init'ed(com.dmdirc.ui.messages.IRCTextAttribute. NICKNAME) |
| presumption | java.text.AttributedCharacterIterator:getAttributes (...)@646 != null |
| presumption | java.text.AttributedCharacterIterator:getAttributes (...)@652 != null |
| presumption | java.text.AttributedCharacterIterator:getAttributes (...)@657 != null |
| presumption | java.text.AttributedString:getIterator(...)@253 != null |
| unanalyzed | call on java.util.Map:entrySet |
| unanalyzed | call on java.util.Set:iterator |
| unanalyzed | call on java.util.Map$Entry:getValue |
| unanalyzed | call on java.util.Map:get |
| unanalyzed | call on java.awt.font.TextLayout:getCharacterCount |
| unanalyzed | call on java.awt.font.TextLayout:hitTestChar |
| unanalyzed | call on java.awt.font.TextHitInfo:getInsertionIndex |
| unanalyzed | call on java.util.Map$Entry:getKey |
| unanalyzed | call on java.awt.Rectangle:contains |
| unanalyzed | call on java.awt.Point:getX |
| unanalyzed | call on java.awt.Point:getY |
| unanalyzed | call on java.util.List:get |
| unanalyzed | call on getStyledLine |
| unanalyzed | call on javax.swing.UIManager:getFont |
| unanalyzed | call on java.awt.Font:getSize |
| unanalyzed | call on com.dmdirc.util.RollingList:contains |
| unanalyzed | call on com.dmdirc.util.RollingList:getList |
| unanalyzed | call on java.util.List:indexOf |
| unanalyzed | call on com.dmdirc.util.RollingList:get |
| unanalyzed | call on com.dmdirc.ui.messages.Styliser:getStyledSt ring |
| unanalyzed | call on javax.swing.text.StyledDocument:getParagrap hElement |
| unanalyzed | call on javax.swing.text.Element:getDocument |
| unanalyzed | call on javax.swing.text.Document:getLength |
| unanalyzed | call on javax.swing.text.Document:getText |
| unanalyzed | call on java.text.AttributedString |
| unanalyzed | call on java.lang.Throwable:__curr_excep_obj |
| unanalyzed | call on javax.swing.text.BadLocationException:getMe ssage |
| unanalyzed | call on com.dmdirc.logger.Logger:userError |
| unanalyzed | call on hasOption |
| unanalyzed | call on java.util.Map:containsKey |
| unanalyzed | call on java.lang.Integer:intValue |
| unanalyzed | call on java.lang.Integer:valueOf |
| unanalyzed | call on java.util.Map:put |
| unanalyzed | call on java.util.List:iterator |
| unanalyzed | call on getOption |
| unanalyzed | call on java.lang.IllegalArgumentException |
| unanalyzed | call on java.lang.String:isEmpty |
| unanalyzed | call on com.dmdirc.util.ConfigFile:getKeyDomain |
| unanalyzed | call on com.dmdirc.util.ConfigFile:isKeyDomain |
| unanalyzed | call on java.awt.Font:getName |
| unanalyzed | call on java.text.AttributedString:getIterator |
| unanalyzed | call on java.text.AttributedCharacterIterator:getEn dIndex |
| unanalyzed | call on java.awt.Font |
| unanalyzed | call on java.text.AttributedString:addAttribute |
| unanalyzed | call on java.awt.Font:getFamily |
| unanalyzed | call on javax.swing.text.Element:getElementCount |
| unanalyzed | call on javax.swing.text.Element:getElement |
| unanalyzed | call on javax.swing.text.Element:getAttributes |
| unanalyzed | call on javax.swing.text.AttributeSet:getAttributeN ames |
| unanalyzed | call on java.util.Enumeration:hasMoreElements |
| unanalyzed | call on java.util.Enumeration:nextElement |
| unanalyzed | call on javax.swing.text.AttributeSet:getAttribute |
| unanalyzed | call on javax.swing.text.Element:getStartOffset |
| unanalyzed | call on javax.swing.text.Element:getEndOffset |
| unanalyzed | call on com.dmdirc.util.RollingList:add |
| test_vector | com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:getCursor(...)@663: Inverse{&new Cursor(TextPaneCanvas__static_init#1)}, Addr_Set{&new Cursor(TextPaneCanvas__static_in it#1)} |
| test_vector | java.util.List:get(...)@89: Addr_Set{null}, Inverse{null} |
| method | void highlightEvent(MouseEventType, MouseEvent) |
| pre | (soft) e != null |
| pre | (soft) this.positions != null |
| pre | (soft) this.selection != null |
| pre | (soft) this.textLayouts != null |
| presumption | com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:getBounds(...)@680 != null |
| presumption | java.awt.event.MouseEvent:getLocationOnScreen(... )@677 != null |
| presumption | java.awt.event.MouseEvent:getPoint(...)@681 != null |
| post | possibly_updated(this.selection.endLine) |
| post | possibly_updated(this.selection.endPos) |
| post | possibly_updated(this.selection.startLine) |
| post | possibly_updated(this.selection.startPos) |
| unanalyzed | call on java.util.Map:entrySet |
| unanalyzed | call on java.util.Set:iterator |
| unanalyzed | call on java.util.Map$Entry:getValue |
| unanalyzed | call on java.util.Map:get |
| unanalyzed | call on java.awt.font.TextLayout:getCharacterCount |
| unanalyzed | call on java.awt.font.TextLayout:hitTestChar |
| unanalyzed | call on java.awt.font.TextHitInfo:getInsertionIndex |
| unanalyzed | call on java.util.Map$Entry:getKey |
| unanalyzed | call on java.awt.Rectangle:contains |
| unanalyzed | call on java.awt.Point:getX |
| unanalyzed | call on java.awt.Point:getY |
| test_vector | com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:contains(...)@679: {1}, {0} |
| test_vector | com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:contains(...)@701: {0}, {1} |
| test_vector | com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:isVisible(...)@676: {0}, {1} |
| method | LineInfo getClickPosition(Point) |
| pre | (soft) this.positions != null |
| pre | (soft) this.textLayouts != null |
| presumption | (int) (java.awt.Point:getX(...)@743) in {-231..232-1} |
| presumption | (int) (java.awt.Point:getY(...)@743) in {-231..232-1} |
| presumption | java.util.Iterator:next(...)@736 != null |
| presumption | java.util.Map:entrySet(...)@736 != null |
| presumption | java.util.Map:get(...)@738 != null |
| presumption | java.util.Map:get(...)@739 != null |
| presumption | java.util.Map_Entry:getKey(...)@737 != null |
| post | return_value == &new LineInfo(getClickPosition# 1) |
| post | new LineInfo(getClickPosition#1) num objects == 1 |
| post | init'ed(return_value.index) |
| post | init'ed(return_value.line) |
| post | init'ed(return_value.part) |
| unanalyzed | call on java.util.Map:entrySet |
| unanalyzed | call on java.util.Set:iterator |
| unanalyzed | call on java.util.Map$Entry:getValue |
| unanalyzed | call on java.util.Map:get |
| unanalyzed | call on java.awt.font.TextLayout:getCharacterCount |
| unanalyzed | call on java.awt.font.TextLayout:hitTestChar |
| unanalyzed | call on java.awt.font.TextHitInfo:getInsertionIndex |
| test_vector | point: Addr_Set{null}, Inverse{null} |
| test_vector | java.awt.Rectangle:contains(...)@737: {0}, {1} |
| test_vector | java.util.Iterator:hasNext(...)@736: {0}, {1} |
| method | LinePosition getSelectedRange() |
| pre | this.selection != null |
| pre | init'ed(this.selection.endLine) |
| pre | init'ed(this.selection.endPos) |
| pre | init'ed(this.selection.startLine) |
| pre | init'ed(this.selection.startPos) |
| post | return_value in Addr_Set{&new LinePosition(getS electedRange#2),&new LinePosition(getSelectedRa nge#3),&new LinePosition(getSelectedRange#1)} |
| post | new LinePosition(getSelectedRange#1) num objects <= 1 |
| post | new LinePosition(getSelectedRange#1).endLine == this.selection.startLine |
| post | new LinePosition(getSelectedRange#1).endLine >= -231+1 |
| post | new LinePosition(getSelectedRange#1).endPos == this.selection.startPos |
| post | init'ed(new LinePosition(getSelectedRange#1). endPos) |
| post | new LinePosition(getSelectedRange#1).startLine == this.selection.endLine |
| post | new LinePosition(getSelectedRange#1).startLine <= 232-2 |
| post | new LinePosition(getSelectedRange#1).startPos == this.selection.endPos |
| post | init'ed(new LinePosition(getSelectedRange#1). startPos) |
| post | new LinePosition(getSelectedRange#2) num objects <= 1 |
| post | new LinePosition(getSelectedRange#2).endLine == this.selection.endLine |
| post | init'ed(new LinePosition(getSelectedRange#2). endLine) |
| post | new LinePosition(getSelectedRange#2).endPos == this.selection.startPos |
| post | new LinePosition(getSelectedRange#2).endPos >= -231+1 |
| post | new LinePosition(getSelectedRange#2).startLine == this.selection.startLine |
| post | init'ed(new LinePosition(getSelectedRange#2). startLine) |
| post | new LinePosition(getSelectedRange#2).startPos == this.selection.endPos |
| post | new LinePosition(getSelectedRange#2).startPos <= 232-2 |
| post | new LinePosition(getSelectedRange#3) num objects <= 1 |
| post | new LinePosition(getSelectedRange#3).endLine == this.selection.endLine |
| post | init'ed(new LinePosition(getSelectedRange#3). endLine) |
| post | new LinePosition(getSelectedRange#3).endPos == this.selection.endPos |
| post | init'ed(new LinePosition(getSelectedRange#3). endPos) |
| post | new LinePosition(getSelectedRange#3).startLine == this.selection.startLine |
| post | init'ed(new LinePosition(getSelectedRange#3). startLine) |
| post | new LinePosition(getSelectedRange#3).startPos == this.selection.startPos |
| post | init'ed(new LinePosition(getSelectedRange#3). startPos) |
| test_vector | this.selection.endLine - this.selection.startLine: {1..6_442_450_943}, {-6_442_450_943..-1}, {0} |
| test_vector | this.selection.endPos - this.selection.startPos: {0..6_442_450_943}, {-6_442_450_943..-1} |