cprover
string_constraint_generator_format.cpp File Reference

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"
Include dependency graph for string_constraint_generator_format.cpp:

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_elementtparse_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...
 

Detailed Description

Generates string constraints for the Java format function.

Definition in file string_constraint_generator_format.cpp.

Function Documentation

◆ format_specifier_of_match()

static string_constraint_generatort::format_specifiert format_specifier_of_match ( std::smatch &  m)
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

Parameters
ma match in a regular expression
Returns
Format specifier represented by the matched string. The groups in the match should represent: index, flag, width, precision, date and conversion type.

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().

◆ get_component_in_struct()

static exprt get_component_in_struct ( const struct_exprt expr,
irep_idt  component_name 
)
static

Helper for add_axioms_for_format_specifier.

Parameters
expra structured expression
component_namename of the desired component
Returns
Expression in the component of 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().

◆ parse_format_string()

static std::vector<format_elementt> parse_format_string ( std::string  s)
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

Parameters
sa string
Returns
A vector of format_elementt.

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().

◆ utf16_constant_array_to_java()

std::string utf16_constant_array_to_java ( const array_exprt arr,
std::size_t  length 
)

Construct a string from a constant array.

Parameters
arran array expression containing only constants
lengthan unsigned value representing the length of the array
Returns
String of length 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_native_endian_to_java().

Referenced by string_constraint_generatort::add_axioms_for_format(), and string_of_array().