cprover
|
Generates string constraints for the Java format function. More...
#include <iomanip>
#include <string>
#include <regex>
#include <vector>
#include <util/std_expr.h>
#include <util/unicode.h>
#include "string_builtin_function.h"
#include "string_constraint_generator.h"
Go to the source code of this file.
Classes | |
class | format_specifiert |
class | format_textt |
class | format_elementt |
Functions | |
static format_specifiert | format_specifier_of_match (std::smatch &m) |
Helper function for parsing format strings. More... | |
static std::vector< format_elementt > | parse_format_string (std::string s) |
Parse the given string into format specifiers and text. More... | |
static exprt | get_component_in_struct (const struct_exprt &expr, irep_idt component_name) |
Helper for add_axioms_for_format_specifier. More... | |
static std::pair< array_string_exprt, string_constraintst > | add_axioms_for_format_specifier (symbol_generatort &fresh_symbol, const format_specifiert &fs, const struct_exprt &arg, const typet &index_type, const typet &char_type, array_poolt &array_pool, const messaget &message, const namespacet &ns) |
Parse s and add axioms ensuring the output corresponds to the output of String.format. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_format (symbol_generatort &fresh_symbol, const array_string_exprt &res, const std::string &s, const exprt::operandst &args, array_poolt &array_pool, const messaget &message, const namespacet &ns) |
Parse s and add axioms ensuring the output corresponds to the output of String.format. More... | |
std::string | utf16_constant_array_to_java (const array_exprt &arr, std::size_t length) |
Construct a string from a constant array. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_format (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const messaget &message, const namespacet &ns) |
Formatted string using a format string and list of arguments. More... | |
Generates string constraints for the Java format function.
Definition in file string_constraint_generator_format.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_format | ( | symbol_generatort & | fresh_symbol, |
const array_string_exprt & | res, | ||
const std::string & | s, | ||
const exprt::operandst & | args, | ||
array_poolt & | array_pool, | ||
const messaget & | message, | ||
const namespacet & | ns | ||
) |
Parse s
and add axioms ensuring the output corresponds to the output of String.format.
fresh_symbol | generator of fresh symbols |
res | string expression for the result of the format function |
s | a format string |
args | a vector of arguments |
array_pool | pool of arrays representing strings |
message | message handler for warnings |
ns | namespace |
Definition at line 381 of file string_constraint_generator_format.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_format | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool, | ||
const messaget & | message, | ||
const namespacet & | ns | ||
) |
Formatted string using a format string and list of arguments.
Add axioms to specify the Java String.format function.
fresh_symbol | generator of fresh symbols |
f | a function application |
array_pool | pool of arrays representing strings |
message | message handler for warnings |
ns | namespace |
Definition at line 510 of file string_constraint_generator_format.cpp.
|
static |
Parse s
and add axioms ensuring the output corresponds to the output of String.format.
Assumes the argument is a structured expression which contains the fields: string expr, int, float, char, boolean, hashcode, date_time. The correct component will be fetched depending on the format specifier.
fresh_symbol | generator of fresh symbols |
fs | a format specifier |
arg | a struct containing the possible value of the argument to format |
index_type | type for indexes in strings |
char_type | type of characters |
array_pool | pool of arrays representing strings |
message | message handler for warnings |
ns | namespace |
Definition at line 260 of file string_constraint_generator_format.cpp.
|
static |
Helper function for parsing format strings.
This follows the implementation in openJDK of the java.util.Formatter class: http://hg.openjdk.java.net/jdk7/jdk7/jdk/file/9b8c96f96a0f/src/share/classes/java/util/Formatter.java#l2660
m | a match in a regular expression |
Definition at line 185 of file string_constraint_generator_format.cpp.
|
static |
Helper for add_axioms_for_format_specifier.
expr | a structured expression |
component_name | name of the desired component |
expr
named component_name
. Definition at line 237 of file string_constraint_generator_format.cpp.
|
static |
Parse the given string into format specifiers and text.
This follows the implementation in openJDK of the java.util.Formatter class: http://hg.openjdk.java.net/jdk7/jdk7/jdk/file/9b8c96f96a0f/src/share/classes/java/util/Formatter.java#l2513
s | a string |
Definition at line 209 of file string_constraint_generator_format.cpp.
std::string utf16_constant_array_to_java | ( | const array_exprt & | arr, |
std::size_t | length | ||
) |
Construct a string from a constant array.
arr | an array expression containing only constants |
length | an unsigned value representing the length of the array |
length
represented by the array assuming each field in arr
represents a character. Definition at line 483 of file string_constraint_generator_format.cpp.