CBMC: /home/runner/work/cbmc/cbmc/src/solvers/strings/string_format_builtin_function.h File Reference

CBMC

Loading...

Searching...

No Matches

Classes | Functions

string_format_builtin_function.h File Reference

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

#include "string_builtin_function.h"

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

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