Skip to content

Add model for String.valueOf(boolean) and StringBuffer.append(boolean) #14

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Nov 20, 2018
Merged

Add model for String.valueOf(boolean) and StringBuffer.append(boolean) #14

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
73b5a1a
Add model for String.valueOf(boolean)
romainbrenguier Nov 20, 2018
d825533
Model for StringBuffer(boolean)
romainbrenguier Nov 20, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 1 addition & 3 deletions src/main/java/java/lang/String.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3873,9 +3873,7 @@ public static String copyValueOf(char data[]) {
* @diffblue.untested
*/
public static String valueOf(boolean b) {
// DIFFBLUE MODEL LIBRARY This is treated internally in CBMC
return CProver.nondetWithoutNullForNotModelled();
// return b ? "true" : "false";
return b ? "true" : "false";
}

/**
Expand Down
4 changes: 2 additions & 2 deletions src/main/java/java/lang/StringBuffer.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -505,11 +505,11 @@ public synchronized StringBuffer append(char[] str, int offset, int len) {
*/
@Override
public synchronized StringBuffer append(boolean b) {
// DIFFBLUE MODEL LIBRARY this is replaced internally
// DIFFBLUE MODEL LIBRARY do not use cache
// toStringCache = null;
// super.append(b);
// return this;
return CProver.nondetWithoutNullForNotModelled();
return append(b ? "true" : "false");
}

/**
Expand Down