Built-in function for String.format(). More...
#include <string_format_builtin_function.h>
get_value which gives a valuation to expressions, attempt to find the result of the builtin function. Built-in function for String.format().
The intent is to support all conversions described in: https://docs.oracle.com/javase/8/docs/api/java/util/Formatter.html#syntax
This table indicates whether each conversion is supported in:
For more information on what these mean, refer to string_builtin_functiont.
| c | SCC | SCE | SL |
|---|---|---|---|
| %b | ✔ | ? | ✔ |
| %B | ? | ? | ✔ |
| %h | ❌ | ❌ | ❌ |
| %H | ❌ | ❌ | ❌ |
| %s | ✔ | ? | ✔ |
| %S | ? | ? | ✔ |
| %c | ? | ? | ✔ |
| %C | ? | ? | ✔ |
| %d | ✔ | ? | ✔ |
| %o | ❌ | ❌ | ❌ |
| %x | ✔ | ✔ | ❌ |
| %X | ? | ✔ | ❌ |
| %e | ? | ❌ | ❌ |
| %E | ? | ❌ | ❌ |
| %f | ? | ❌ | ❌ |
| %g | ❌ | ❌ | ❌ |
| %G | ❌ | ❌ | ❌ |
| %a | ❌ | ❌ | ❌ |
| %A | ❌ | ❌ | ❌ |
| %t | ❌ | ❌ | ❌ |
| %T | ❌ | ❌ | ❌ |
| %% | ✔ | ? | ✔ |
| %n | ✔ | ? | ✔ |
✓ = full support, ? = untested support , ❌ = no support
The index component of the formatter is supported, but the other components (flag, width, precision, dt) are ignored.
Definition at line 62 of file string_format_builtin_function.h.
Constructor from arguments of a function application.
The arguments in fun_args should be in order: an integer result.length, a character pointer &result[0], a string of type refined_string_typet for the format string, any number of strings of type refined_string_typet.
Definition at line 29 of file string_format_builtin_function.cpp.
Add constraints ensuring that the value of result expression of the builtin function corresponds to the value of the function call.
The constraints are only added when deemed necessary, i.e. when maybe_testing_function() returns true, or when testing function depends on the result of this function. This logic is implemented in add_constraints().
Implements string_builtin_functiont.
Definition at line 589 of file string_format_builtin_function.cpp.
Given a function get_value which gives a valuation to expressions, attempt to find the result of the builtin function.
If not enough information can be gathered from get_value, return an empty optional.
Implements string_builtin_functiont.
Definition at line 519 of file string_format_builtin_function.cpp.
Constraint ensuring that the length of the strings are coherent with the function call.
Implements string_builtin_functiont.
Definition at line 766 of file string_format_builtin_function.cpp.
In principle this function could return true, because the content of the string sometimes needs to be propagated.
This is the case for methods under test that have a test on the length of the formatted string, which may depend on the content of the string. For instance, if the format string contains a boolean formatter, the length of the resulting string depends on the value of the argument (true or false, with respective lengths of 4 and 5), which needs to be propagated. Since propagating these constraints is costly and unnecessary in most cases, we set the function to return false, and rely on the user to propagate the constants explicitly, as it is done in the cproverFormatArgument method of lib/cbmc/jbmc/lib/java-models-library/src/main/java/java/lang/String.java
Reimplemented from string_builtin_functiont.
Definition at line 118 of file string_format_builtin_function.h.
Implements string_builtin_functiont.
Definition at line 94 of file string_format_builtin_function.h.
Reimplemented from string_builtin_functiont.
Definition at line 86 of file string_format_builtin_function.h.
Reimplemented from string_builtin_functiont.
Definition at line 81 of file string_format_builtin_function.h.
Only set when the format string is a constant.
In the other case, the result will be non-deterministic
Definition at line 68 of file string_format_builtin_function.h.
Definition at line 69 of file string_format_builtin_function.h.
Definition at line 65 of file string_format_builtin_function.h.