cprover
Loading...
Searching...
No Matches
string_format_builtin_function.cpp File Reference

Built-in function for String.format. More...

#include <iterator>
#include <string>
#include "format_specifier.h"
#include "string_format_builtin_function.h"
#include "string_refinement_util.h"
#include <util/bitvector_expr.h>
#include <util/message.h>
#include <util/range.h>
#include <util/simplify_expr.h>
Include dependency graph for string_format_builtin_function.cpp:

Go to the source code of this file.

Functions

static exprt format_arg_from_string (const array_string_exprt &string, const irep_idt &id, array_poolt &array_pool)
 Deserialize an argument for format from string.
static exprt is_null (const array_string_exprt &string, array_poolt &array_pool)
 Expression which is true when the string is equal to the literal "null".
static std::pair< array_string_exprt, string_constraintstadd_axioms_for_format_specifier (string_constraint_generatort &generator, const format_specifiert &fs, const array_string_exprt &string_arg, const typet &index_type, const typet &char_type, message_handlert &message_handler)
 Parse s and add axioms ensuring the output corresponds to the output of String.format.
static std::pair< exprt, string_constraintstadd_axioms_for_format (string_constraint_generatort &generator, const array_string_exprt &res, const std::string &s, const std::vector< array_string_exprt > &args, message_handlert &message_handler)
 Parse s and add axioms ensuring the output corresponds to the output of String.format.
static std::vector< mp_integerdeserialize_constant_int_arg (const std::vector< mp_integer > serialized, const unsigned base)
static bool eval_is_null (const std::vector< mp_integer > &string)
static std::vector< mp_integereval_format_specifier (const format_specifiert &fs, const std::vector< mp_integer > &arg)
 Return the string to replace the format specifier, as a vector of characters.
static exprt length_of_positive_decimal_int (const exprt &pos_integer, int max_length, const typet &length_type, const unsigned long radix)
 Return an new expression representing the length of the representation of integer.
exprt length_of_decimal_int (const exprt &integer, const typet &length_type, const unsigned long radix)
 Compute the length of the decimal representation of an integer.
exprt length_for_format_specifier (const format_specifiert &fs, const array_string_exprt &arg, const typet &index_type, array_poolt &array_pool)
 Return an expression representing the length of the format specifier Does not assume that arg is constant.

Detailed Description

Built-in function for String.format.

Definition in file string_format_builtin_function.cpp.

Function Documentation

◆ add_axioms_for_format()

std::pair< exprt, string_constraintst > add_axioms_for_format ( string_constraint_generatort & generator,
const array_string_exprt & res,
const std::string & s,
const std::vector< array_string_exprt > & args,
message_handlert & message_handler )
static

Parse s and add axioms ensuring the output corresponds to the output of String.format.

Parameters
generatorconstraint generator
resstring expression for the result of the format function
sa format string
argsa vector of arguments
message_handlermessage handler for warnings
Returns
code, 0 on success

Definition at line 297 of file string_format_builtin_function.cpp.

◆ add_axioms_for_format_specifier()

std::pair< array_string_exprt, string_constraintst > add_axioms_for_format_specifier ( string_constraint_generatort & generator,
const format_specifiert & fs,
const array_string_exprt & string_arg,
const typet & index_type,
const typet & char_type,
message_handlert & message_handler )
static

Parse s and add axioms ensuring the output corresponds to the output of String.format.

Assumes the argument is a string representing one of: string expr, int, float, char, boolean, hashcode, date_time. The correct type will be retrieved by calling get_arg with an id depending on the format specifier.

Parameters
generatorconstraint generator
fsa format specifier
string_argformat string from argument
index_typetype for indexes in strings
char_typetype of characters
message_handlermessage handler for warnings
Returns
String expression representing the output of String.format.

Definition at line 118 of file string_format_builtin_function.cpp.

◆ deserialize_constant_int_arg()

std::vector< mp_integer > deserialize_constant_int_arg ( const std::vector< mp_integer > serialized,
const unsigned base )
static

Definition at line 399 of file string_format_builtin_function.cpp.

◆ eval_format_specifier()

std::vector< mp_integer > eval_format_specifier ( const format_specifiert & fs,
const std::vector< mp_integer > & arg )
static

Return the string to replace the format specifier, as a vector of characters.

Definition at line 431 of file string_format_builtin_function.cpp.

◆ eval_is_null()

bool eval_is_null ( const std::vector< mp_integer > & string)
static

Definition at line 423 of file string_format_builtin_function.cpp.

◆ format_arg_from_string()

exprt format_arg_from_string ( const array_string_exprt & string,
const irep_idt & id,
array_poolt & array_pool )
static

Deserialize an argument for format from string.

id should be one of: string_expr, int, char, boolean, float. The primitive values are expected to all be encoded using 4 characters. The characters of string must be of type unsignedbv_typet(16).

Definition at line 243 of file string_format_builtin_function.cpp.

◆ is_null()

exprt is_null ( const array_string_exprt & string,
array_poolt & array_pool )
static

Expression which is true when the string is equal to the literal "null".

Definition at line 94 of file string_format_builtin_function.cpp.

◆ length_for_format_specifier()

exprt length_for_format_specifier ( const format_specifiert & fs,
const array_string_exprt & arg,
const typet & index_type,
array_poolt & array_pool )

Return an expression representing the length of the format specifier Does not assume that arg is constant.

Definition at line 684 of file string_format_builtin_function.cpp.

◆ length_of_decimal_int()

exprt length_of_decimal_int ( const exprt & integer,
const typet & length_type,
const unsigned long radix )

Compute the length of the decimal representation of an integer.

Parameters
integer(not necessarily constant) integer for which to compute the length of the decimal representation.
length_typetype to give to the created expression
radixradix of the output representation.
Returns
: An exprt representing the length of integer

Definition at line 651 of file string_format_builtin_function.cpp.

◆ length_of_positive_decimal_int()

exprt length_of_positive_decimal_int ( const exprt & pos_integer,
int max_length,
const typet & length_type,
const unsigned long radix )
static

Return an new expression representing the length of the representation of integer.

If max_length is less than the length of integer, the returned expression will represent max_length.

Parameters
pos_integerpositive (but not necessarily constant) integer for which to compute the length of the decimal representation.
max_lengthmax length of the decimal representation. If max_length is less than the length of integer, the returned expression will represent max_length. Choosing a value greater than the actual max possible length is harmless but will result in useless constraints.
length_typetype to give to the created expression
radixradix of the output representation.
Returns
: An exprt representing the length of integer

Definition at line 623 of file string_format_builtin_function.cpp.