string_format_builtin_function.cpp File Reference

#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. More...
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". More...
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. More...
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. More...
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. More...
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. More...
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. More...
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. More...

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 296 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 398 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 430 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 422 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 242 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 683 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 650 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 622 of file string_format_builtin_function.cpp.