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_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)

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

static 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)

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

static std::vector< mp_integer > deserialize_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_integer > eval_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()

static 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: generator constraint generator

res string expression for the result of the format function

s a format string

args a vector of arguments

message_handler message handler for warnings

Returns: code, 0 on success

Definition at line 297 of file string_format_builtin_function.cpp.

◆ add_axioms_for_format_specifier()

static 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: generator constraint generator

fs a format specifier

string_arg format string from argument

index_type type for indexes in strings

char_type type of characters

message_handler message 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()

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

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

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

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

static 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_type type to give to the created expression

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

static 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_integer positive (but not necessarily constant) integer for which to compute the length of the decimal representation.

max_length max 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_type type to give to the created expression

radix radix of the output representation.

Returns: : An exprt representing the length of integer

Definition at line 623 of file string_format_builtin_function.cpp.