Built-in function for String.format(). More...
#include <string_format_builtin_function.h>
Inheritance diagram for string_format_builtin_functiont: Collaboration diagram for string_format_builtin_functiont:Public Member Functions | |
| string_format_builtin_functiont (const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool) | |
| Constructor from arguments of a function application. More... | |
| std::optional< array_string_exprt > | string_result () const override |
| std::vector< array_string_exprt > | string_arguments () const override |
| std::optional< exprt > | eval (const std::function< exprt(const exprt &)> &get_value) const override |
Given a function get_value which gives a valuation to expressions, attempt to find the result of the builtin function. More... | |
| std::string | name () const override |
| string_constraintst | constraints (string_constraint_generatort &generator, message_handlert &message_handler) const override |
| Add constraints ensuring that the value of result expression of the builtin function corresponds to the value of the function call. More... | |
| exprt | length_constraint () const override |
| Constraint ensuring that the length of the strings are coherent with the function call. More... | |
| bool | maybe_testing_function () const override |
| In principle this function could return true, because the content of the string sometimes needs to be propagated. More... | |
| Public Member Functions inherited from string_builtin_functiont | |
| string_builtin_functiont ()=delete | |
| string_builtin_functiont (const string_builtin_functiont &)=delete | |
| virtual | ~string_builtin_functiont ()=default |
Public Attributes | |
| array_string_exprt | result |
| std::optional< std::string > | format_string |
| Only set when the format string is a constant. More... | |
| std::vector< array_string_exprt > | inputs |
| Public Attributes inherited from string_builtin_functiont | |
| exprt | return_code |
Additional Inherited Members | |
| Protected Member Functions inherited from string_builtin_functiont | |
| string_builtin_functiont (exprt return_code, array_poolt &array_pool) | |
| Protected Attributes inherited from string_builtin_functiont | |
| array_poolt & | array_pool |
Detailed Description
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:
- string content constraint generation (SCC)
- string content evaluation (SCE)
- string length constraint generation (SL)
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 & Destructor Documentation
◆ string_format_builtin_functiont()
| string_format_builtin_functiont::string_format_builtin_functiont | ( | const exprt & | return_code, |
| const std::vector< exprt > & | fun_args, | ||
| array_poolt & | array_pool | ||
| ) |
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.
Member Function Documentation
◆ constraints()
|
overridevirtual |
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.
◆ eval()
|
overridevirtual |
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.
◆ length_constraint()
|
overridevirtual |
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.
◆ maybe_testing_function()
|
inlineoverridevirtual |
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.
◆ name()
|
inlineoverridevirtual |
Implements string_builtin_functiont.
Definition at line 94 of file string_format_builtin_function.h.
◆ string_arguments()
|
inlineoverridevirtual |
Reimplemented from string_builtin_functiont.
Definition at line 86 of file string_format_builtin_function.h.
◆ string_result()
|
inlineoverridevirtual |
Reimplemented from string_builtin_functiont.
Definition at line 81 of file string_format_builtin_function.h.
Member Data Documentation
◆ format_string
| std::optional<std::string> string_format_builtin_functiont::format_string |
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.
◆ inputs
| std::vector<array_string_exprt> string_format_builtin_functiont::inputs |
Definition at line 69 of file string_format_builtin_function.h.
◆ result
| array_string_exprt string_format_builtin_functiont::result |
Definition at line 65 of file string_format_builtin_function.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/solvers/strings/string_format_builtin_function.h
- /home/runner/work/cbmc/cbmc/src/solvers/strings/string_format_builtin_function.cpp
