CBMC
string_format_builtin_function.h File Reference

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

+ Include dependency graph for string_format_builtin_function.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  string_format_builtin_functiont
 Built-in function for String.format(). More...
 

Functions

exprt length_of_decimal_int (const exprt &integer, const typet &length_type, const unsigned long base)
 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.h.

Function Documentation

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