Repository navigation
Model additions from SV-COMP 26 - #48
peterschrammel wants to merge 6 commits into
Conversation
as required by LinkedList
and its dependencies
| static Class getPrimitiveClass(int i){ | ||
| if(i==0) | ||
| return Class.forName("boolean"); | ||
| return boolean.class; |
There was a problem hiding this comment.
int.class compiles to getstatic Integer.TYPE, so Integer.<clinit> reads Integer.TYPE while initialising it: all TYPE fields end up null (assert Integer.TYPE != null fails). getPrimitiveClass(String) (Character) still uses forName. Drop this commit in favour of #43?
| */ | ||
| public PrintWriter printf(String format, Object ... args) { | ||
| // return format(format, args); | ||
| return CProver.nondetWithoutNull(this); |
There was a problem hiding this comment.
nondetWithoutNull(this) ignores its argument and returns a fresh object; should be return this; (also lines 990, 1053, 1116, 1152, 1194, 1219). pw.append('a') == pw currently fails.
| public class Collections { | ||
| // Suppresses default constructor, ensuring non-instantiability. | ||
| // DIFFBLUE MODEL LIBRARY - not used in model | ||
| // private Collections() { |
There was a problem hiding this comment.
Keep the private constructor: without it, Collections gets a public one.
| */ | ||
| @SuppressWarnings("unchecked") | ||
| public static <T extends Comparable<? super T>> void sort(List<T> list) { | ||
| list.sort(null); |
There was a problem hiding this comment.
ArrayList.sort is notModelled, which JBMC treats as a no-op, so this doesn't sort: after sorting [3, 1], assert l.get(0) == 3 is SUCCESSFUL. Not fullSupport.
| * @diffblue.untested | ||
| * @diffblue.noSupport | ||
| */ | ||
| public static <T> void fill(List<? super T> list, T obj) { |
There was a problem hiding this comment.
notModelled in a void method is a no-op, so fill silently does nothing (wrong SUCCESS). Keep the JDK body? Same for other simple void methods.
| // return a; | ||
| if (a.length < size()) { | ||
| // DIFFBLUE MODEL LIBRARY | ||
| // Object.getClass() is currently not modelled, so we need to use |
There was a problem hiding this comment.
Out of date once diffblue/cbmc#9390 is merged.
| * | ||
| * @diffblue.noSupport | ||
| */ | ||
| public void write(String str) throws IOException { |
There was a problem hiding this comment.
No-op, so a user's Writer subclass never sees this reach its write(char[], int, int). The JDK bodies of write(String), write(char[]) and append only delegate; keep them?
| * @diffblue.untested Only exception support is tested. | ||
| * */ | ||
| @Override | ||
| public char charAt(int index) { |
There was a problem hiding this comment.
What does this fix? JBMC's string solver replaces StringBuilder.charAt:(I)C anyway; I saw no difference, with or without --no-refine-strings.
| * | ||
| * @since 1.5 | ||
| */ | ||
|
|
There was a problem hiding this comment.
Nit: the only change from OpenJDK.
| * @author Josh Bloch | ||
| * @since 1.7 | ||
| */ | ||
|
|
There was a problem hiding this comment.
Nit: the only change from OpenJDK.
No description provided.