| method | String getLookAndFeel(String) |
| presumption | arr$.length@150 <= 232-1 |
| presumption | arr$[i$]@150 != null |
| presumption | javax.swing.UIManager:getInstalledLookAndFeels(... )@150 != null |
| presumption | javax.swing.UIManager_LookAndFeelInfo:getName(... )@151 != null |
| post | java.lang.StringBuilder:toString(...)._tainted == 0 |
| post | init'ed(return_value) |
| test_vector | displayName: Addr_Set{null}, Inverse{null} |
| test_vector | java.lang.String:equals(...)@143: {0}, {1} |
| test_vector | java.lang.String:equals(...)@151: {0}, {1} |
| test_vector | java.lang.String:isEmpty(...)@143: {1}, {0} |
| test_vector | java.lang.StringBuilder:length(...)@157: {-231..-1, 1..232-1}, {0} |
| method | String clipStringifNeeded(JComponent, String, int) |
| pre | (soft) component != null |
| post | init'ed(java.lang.StringBuilder:toString(...)._ tainted) |
| post | return_value == One-of{&"", &java.lang. StringBuilder:toString(...), string} |
| post | return_value != null |
| unanalyzed | call on java.lang.String:equals |
| unanalyzed | call on javax.swing.JComponent:getFont |
| unanalyzed | call on javax.swing.JComponent:getFontMetrics |
| unanalyzed | call on javax.swing.SwingUtilities:computeStringWid th |
| unanalyzed | call on java.lang.String:length |
| unanalyzed | call on java.lang.String:charAt |
| unanalyzed | call on java.awt.FontMetrics:charWidth |
| unanalyzed | call on java.lang.String:substring |
| test_vector | string: Addr_Set{null}, Inverse{null} |
| test_vector | java.lang.String:equals(...)@292: {0}, {1} |
| method | String clipString(JComponent, String, int) |
| pre | (soft) component != null |
| presumption | javax.swing.JComponent:getFontMetrics(...)@316 != null |
| post | init'ed(java.lang.StringBuilder:toString(...)._ tainted) |
| post | return_value in Addr_Set{&"",&java.lang. StringBuilder:toString(...)} |
| test_vector | string: Addr_Set{null}, Inverse{null} |
| test_vector | java.lang.String:equals(...)@313: {0}, {1} |