From 73b5a1ac47f61bc34edc29a7203c0f4418315054 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 20 Nov 2018 10:35:44 +0000 Subject: [PATCH 1/2] Add model for String.valueOf(boolean) --- src/main/java/java/lang/String.java | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/main/java/java/lang/String.java b/src/main/java/java/lang/String.java index 0bd0854..8f4527e 100644 --- a/src/main/java/java/lang/String.java +++ b/src/main/java/java/lang/String.java @@ -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"; } /** From d825533d7feaa477dba880abd679805dede9bb4e Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 20 Nov 2018 10:45:33 +0000 Subject: [PATCH 2/2] Model for StringBuffer(boolean) --- src/main/java/java/lang/StringBuffer.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/java/java/lang/StringBuffer.java b/src/main/java/java/lang/StringBuffer.java index 7d3c120..b89d4e4 100644 --- a/src/main/java/java/lang/StringBuffer.java +++ b/src/main/java/java/lang/StringBuffer.java @@ -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"); } /**