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_constraint_generator.h"
Go to the source code of this file.
Classes | |
class | string_constraint_generatort::format_specifiert |
class | format_textt |
class | format_elementt |
Functions | |
static string_constraint_generatort::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... | |
std::string | utf16_constant_array_to_java (const array_exprt &arr, std::size_t length) |
Construct a string from a constant array. More... | |
Generates string constraints for the Java format function.
Definition in 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 187 of file string_constraint_generator_format.cpp.
References string_constraint_generatort::format_specifiert::DATE_TIME_UPPER, and INVARIANT.
Referenced by parse_format_string().
|
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 241 of file string_constraint_generator_format.cpp.
References struct_union_typet::component_number(), exprt::operands(), to_struct_type(), and exprt::type().
Referenced by string_constraint_generatort::add_axioms_for_format_specifier().
|
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 213 of file string_constraint_generator_format.cpp.
References format_specifier_of_match().
Referenced by string_constraint_generatort::add_axioms_for_format().
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 435 of file string_constraint_generator_format.cpp.
References INVARIANT, exprt::operands(), PRECONDITION, to_constant_expr(), to_unsigned_integer(), and utf16_little_endian_to_java().
Referenced by string_constraint_generatort::add_axioms_for_format(), and string_of_array().