printf_formattert Class Reference

#include <printf_formatter.h>

Classes
class	eol_exception

Public Member Functions
void	operator() (const std::string &format, const std::list< expr2tc > &_operands)
void	print (std::ostream &out)
std::string	as_string ()

Public Attributes
size_t	min_outlen = 0
	Minimum possible output length for the last print() call.
size_t	max_outlen = 0
	Maximum possible output length for the last print() call.
bool	bounded = true
	False when print() could not compute a sound upper bound on the output length: a value-dependent conversion (s, e/f/g) was given a non-constant argument, or an expected argument was missing.
bool	exact = true
	False when a '#' flag outside o, x and X or a conversion (p, an unknown one) the formatter does not model appeared, so the text it produced may differ from the real output.
bool	args_reliable = true
	True when operands are the call's actual arguments, so a non-literal s operand may be used to derive a sound object-size length bound.

Protected Member Functions
bool	eol () const
char	next ()
void	process_char (std::ostream &out)
void	process_format (std::ostream &out)
const expr2tc	make_type (const expr2tc &src, const type2tc &dest)

Protected Attributes
std::string	format
std::list< expr2tc >	operands
std::list< expr2tc >::const_iterator	next_operand
unsigned	format_pos

Member Function Documentation

as_string()

std::string printf_formattert::as_string

(

)

eol()

bool printf_formattert::eol ( ) const

inlineprotected

make_type()

const expr2tc printf_formattert::make_type ( const expr2tc & src, const type2tc & dest )

protected

next()

char printf_formattert::next ( )

inlineprotected

operator()()

void printf_formattert::operator()	(	const std::string &	format,
		const std::list< expr2tc > &	_operands )

print()

void printf_formattert::print

(

std::ostream &

out

)

process_char()

void printf_formattert::process_char ( std::ostream & out )

protected

process_format()

void printf_formattert::process_format ( std::ostream & out )

protected

Member Data Documentation

args_reliable

bool printf_formattert::args_reliable = true

True when operands are the call's actual arguments, so a non-literal s operand may be used to derive a sound object-size length bound.

For the v* variants (vprintf/vsprintf/vsnprintf/vasprintf/vfprintf) the arguments are hidden behind a va_list and the operand at a s position is the va_list itself, not the string — deriving a size bound from it would be unsound, so callers set this false and s stays unbounded.

bounded

bool printf_formattert::bounded = true

False when print() could not compute a sound upper bound on the output length: a value-dependent conversion (s, e/f/g) was given a non-constant argument, or an expected argument was missing.

When false, max_outlen is NOT a valid upper bound and callers must treat the return value as unbounded (unconstrained nondet). Always true after a run over a format whose conversions are all constant-bounded.

exact

bool printf_formattert::exact = true

False when a '#' flag outside o, x and X or a conversion (p, an unknown one) the formatter does not model appeared, so the text it produced may differ from the real output.

format

std::string printf_formattert::format

protected

format_pos

unsigned printf_formattert::format_pos

protected

max_outlen

size_t printf_formattert::max_outlen = 0

Maximum possible output length for the last print() call.

min_outlen

size_t printf_formattert::min_outlen = 0

Minimum possible output length for the last print() call.

Equals max_outlen when all format arguments are constants.

next_operand

std::list<expr2tc>::const_iterator printf_formattert::next_operand

protected

operands

std::list<expr2tc> printf_formattert::operands

protected

---

The documentation for this class was generated from the following files:

• src/goto-symex/trace/printf_formatter.h
• src/goto-symex/trace/printf_formatter.cpp