-
Notifications
You must be signed in to change notification settings - Fork 277
Adding support for String.format function #1105
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.
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
romainbrenguier
merged 14 commits into
diffblue:test-gen-support
from
romainbrenguier:feature/string-format
Aug 1, 2017
Merged
Changes from all commits
Commits
Show all changes
14 commits
Select commit
Hold shift + click to select a range
760e6bd
Adding intermediary function for empty strings
romainbrenguier b4b0a6e
Intermediary function for conversion to uppercase
romainbrenguier f8d54e3
New file for String.format function
romainbrenguier 9bcb2e7
Adding declaration of format functions and string_of_constant_array
romainbrenguier c79baf8
Factorizing part of string_of_array in string_refiniment with code of…
romainbrenguier 162b45b
Adding calls to add_axioms_for_format in add_axioms_for_function_appl…
romainbrenguier 2d6d689
Adding String.format to Java String library preprocessing
romainbrenguier 27be555
Adding test for String.format function
romainbrenguier 6fd1c32
Renaming utility function to utf16_constant_array_to_ascii
romainbrenguier c7d972f
Corrections in string refinement constraint generation
romainbrenguier bf0c217
Adding test for String.format with non-constant argument
romainbrenguier 5138f7d
Adding a test with an indexed argument in format
romainbrenguier 1d99413
Adding test for exception throwing in String.format
romainbrenguier ceb8ab7
Adding a test with multiple arguments
romainbrenguier File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
Binary file not shown.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
CORE | ||
test.class | ||
--refine-strings --string-max-length 20 | ||
^EXIT=10$ | ||
^SIGNAL=0$ | ||
^\[.*assertion.1\].* line 6.* SUCCESS$ | ||
^\[.*assertion.2\].* line 7.* FAILURE$ | ||
-- |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
public class test | ||
{ | ||
public static String main() | ||
{ | ||
String s = String.format("foo %s", "bar"); | ||
assert(s.equals("foo bar")); | ||
assert(!s.equals("foo bar")); | ||
return s; | ||
} | ||
} | ||
Binary file not shown.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
CORE | ||
test.class | ||
--refine-strings --string-max-length 20 | ||
^EXIT=10$ | ||
^SIGNAL=0$ | ||
^\[.*assertion.1\].* line 6.* SUCCESS$ | ||
^\[.*assertion.2\].* line 7.* FAILURE$ | ||
-- |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
public class test | ||
{ | ||
public static String main(String str) | ||
{ | ||
String s = String.format("foo %s", str); | ||
assert(s.equals("foo ".concat(str))); | ||
assert(!s.equals("foo ".concat(str))); | ||
return s; | ||
} | ||
} |
Binary file not shown.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
CORE | ||
test.class | ||
--refine-strings --string-max-length 20 | ||
^EXIT=10$ | ||
^SIGNAL=0$ | ||
^\[.*assertion.1\].* line 7.* SUCCESS$ | ||
^\[.*assertion.2\].* line 9.* FAILURE$ | ||
-- |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
public class test | ||
{ | ||
public static String main(int i) | ||
{ | ||
String s = String.format("%3$sar", "a", "r", "b"); | ||
if(i==0) | ||
assert(s.equals("bar")); | ||
else | ||
assert(!s.equals("bar")); | ||
return s; | ||
} | ||
} |
Binary file not shown.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
KNOWNBUG | ||
test.class | ||
--refine-strings --string-max-length 20 | ||
^EXIT=10$ | ||
^SIGNAL=0$ | ||
^\[.*assertion.1\].* line 8.* SUCCESS$ | ||
^\[.*assertion.2\].* line 13.* FAILURE$ | ||
-- |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,17 @@ | ||
public class test | ||
{ | ||
public static String main(String str) | ||
{ | ||
try | ||
{ | ||
String s = String.format("%s %s", "a"); | ||
assert(false); | ||
return s; | ||
} | ||
catch(java.util.IllegalFormatException e) | ||
{ | ||
assert(false); | ||
return str; | ||
} | ||
} | ||
} |
Binary file not shown.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
THOROUGH | ||
test.class | ||
--refine-strings --string-max-length 20 | ||
^EXIT=10$ | ||
^SIGNAL=0$ | ||
^\[.*assertion.1\].* line 7.* SUCCESS$ | ||
^\[.*assertion.2\].* line 9.* FAILURE$ | ||
-- |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
public class test | ||
{ | ||
public static String main(boolean b) | ||
{ | ||
String s = String.format("%s%s%s%s%s%s%s%s", "a", "b", "c", "d", "e", "f", "g", "h"); | ||
if(b) | ||
assert(s.equals("abcdefgh")); | ||
else | ||
assert(!s.equals("abcdefgh")); | ||
return s; | ||
} | ||
} |
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
How does this behave with non-constant arguments?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I added a test where the second argument is not constant and this works fine
When the first argument of format (the format specifier) is not constant then the result should be non-deterministic I can add an example of that (marked as KNOWNBUG) and some others with indexes, and more than 10 arguments for example.