replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

added stringBuilder methods insert, delete and deleteCharAt 

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
This commit is contained in:
Lucas Cordeiro 2017-02-22 14:19:25 +00:00
parent 8ec8477053
commit 7e742bc8ad
9 changed files with 153 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

BIN
regression/strings/StringBuilderInsertDelete01/StringBuilderInsertDelete01.class Normal file
View File

Binary file not shown.

46
regression/strings/StringBuilderInsertDelete01/StringBuilderInsertDelete01.java Normal file
View File

@ -0,0 +1,46 @@
public class StringBuilderInsertDelete01
{
public static void main(String[] args)
{
Object objectRef = "diffblue";
String string = "test";
char[] charArray = {'v', 'e', 'r', 'i', 'f', 'i', 'c', 'a', 't', 'i', 'o', 'n'};
boolean booleanValue = true;
char characterValue = 'K';
int integerValue = 7;
long longValue = 10000000;
float floatValue = 2.5f;
double doubleValue = 33.333;
StringBuilder buffer = new StringBuilder();
buffer.insert(0, objectRef)
.insert(0, "-")
.insert(0, string)
.insert(0, "-")
.insert(0, charArray)
.insert(0, "-")
.insert(0, charArray, 3, 3)
.insert(0, "-")
.insert(0, booleanValue)
.insert(0, "-")
.insert(0, characterValue)
.insert(0, "-")
.insert(0, integerValue)
.insert(0, "-")
.insert(0, longValue)
.insert(0, "-")
.insert(0, floatValue)
.insert(0, "-")
.insert(0, doubleValue);
String tmp=buffer.toString();
assert tmp.equals("33.333-2.5-10000000-7-K-true-ifi-verification-test-diffblue");
buffer.deleteCharAt(10);
buffer.delete(2, 6);
tmp=buffer.toString();
assert tmp.equals("33-2.510000000-7-K-true-ifi-verification-test-diffblue");
}
}

8
regression/strings/StringBuilderInsertDelete01/test.desc Normal file
View File

@ -0,0 +1,8 @@
FUTURE
StringBuilderInsertDelete01.class
--string-refine
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring

BIN
regression/strings/StringBuilderInsertDelete02/StringBuilderInsertDelete02.class Normal file
View File

Binary file not shown.

40
regression/strings/StringBuilderInsertDelete02/StringBuilderInsertDelete02.java Normal file
View File

@ -0,0 +1,40 @@
public class StringBuilderInsertDelete02
{
public static void main(String[] args)
{
Object objectRef = "diffblue";
String string = "test";
char[] charArray = {'v', 'e', 'r', 'i', 'f', 'i', 'c', 'a', 't', 'i', 'o', 'n'};
boolean booleanValue = true;
char characterValue = 'K';
int integerValue = 7;
long longValue = 10000000;
float floatValue = 2.5f;
double doubleValue = 33.333;
StringBuilder buffer = new StringBuilder();
buffer.insert(0, objectRef)
.insert(0, "-")
.insert(0, string)
.insert(0, "-")
.insert(0, charArray)
.insert(0, "-")
.insert(0, charArray, 3, 3)
.insert(0, "-")
.insert(0, booleanValue)
.insert(0, "-")
.insert(0, characterValue)
.insert(0, "-")
.insert(0, integerValue)
.insert(0, "-")
.insert(0, longValue)
.insert(0, "-")
.insert(0, floatValue)
.insert(0, "-")
.insert(0, doubleValue);
String tmp=buffer.toString();
assert tmp.equals("33.333-2.5-10000000-7-K-true-ifi-verification-test--diffblue");
}
}

8
regression/strings/StringBuilderInsertDelete02/test.desc Normal file
View File

@ -0,0 +1,8 @@
FUTURE
StringBuilderInsertDelete02.class
--string-refine
^EXIT=0$
^SIGNAL=0$
^VERIFICATION FAILED$
--
^warning: ignoring

BIN
regression/strings/StringBuilderInsertDelete03/StringBuilderInsertDelete03.class Normal file
View File

Binary file not shown.

43
regression/strings/StringBuilderInsertDelete03/StringBuilderInsertDelete03.java Normal file
View File

@ -0,0 +1,43 @@
public class StringBuilderInsertDelete03
{
public static void main(String[] args)
{
Object objectRef = "diffblue";
String string = "test";
char[] charArray = {'v', 'e', 'r', 'i', 'f', 'i', 'c', 'a', 't', 'i', 'o', 'n'};
boolean booleanValue = true;
char characterValue = 'K';
int integerValue = 7;
long longValue = 10000000;
float floatValue = 2.5f;
double doubleValue = 33.333;
StringBuilder buffer = new StringBuilder();
buffer.insert(0, objectRef)
.insert(0, "-")
.insert(0, string)
.insert(0, "-")
.insert(0, charArray)
.insert(0, "-")
.insert(0, charArray, 3, 3)
.insert(0, "-")
.insert(0, booleanValue)
.insert(0, "-")
.insert(0, characterValue)
.insert(0, "-")
.insert(0, integerValue)
.insert(0, "-")
.insert(0, longValue)
.insert(0, "-")
.insert(0, floatValue)
.insert(0, "-")
.insert(0, doubleValue);
buffer.deleteCharAt(10);
buffer.delete(2, 6);
String tmp=buffer.toString();
assert tmp.equals("33-2.510000000-7-K-true-iai-verification-test-diffblue");
}
}

8
regression/strings/StringBuilderInsertDelete03/test.desc Normal file
View File

@ -0,0 +1,8 @@
FUTURE
StringBuilderInsertDelete03.class
--string-refine
^EXIT=0$
^SIGNAL=0$
^VERIFICATION FAILED$
--
^warning: ignoring