java_string_library_preprocess.h File Reference

Produce code for simple implementation of String Java libraries. More...

#include <util/ui_message.h>
#include <util/std_code.h>
#include <util/symbol_table.h>
#include <util/refined_string_type.h>
#include <util/string_expr.h>
#include <util/ieee_float.h>
#include <array>
#include <unordered_set>
#include <functional>
#include "character_refine_preprocess.h"
#include "java_types.h"

Include dependency graph for java_string_library_preprocess.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	java_string_library_preprocesst

Macros
#define	MAX_FORMAT_ARGS   10

Functions
exprt	make_nondet_infinite_char_array (symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
	Declare a fresh symbol of type array of character with infinite size. More...
void	add_pointer_to_array_association (const exprt &pointer, const exprt &array, symbol_table_baset &symbol_table, const source_locationt &loc, code_blockt &code)
	Add a call to a primitive of the string solver, letting it know that pointer points to the first character of array. More...
void	add_array_to_length_association (const exprt &array, const exprt &length, symbol_table_baset &symbol_table, const source_locationt &loc, code_blockt &code)
	Add a call to a primitive of the string solver, letting it know that the actual length of array is length. More...
void	add_character_set_constraint (const exprt &pointer, const exprt &length, const irep_idt &char_set, symbol_table_baset &symbol_table, const source_locationt &loc, code_blockt &code)
	Add a call to a primitive of the string solver which ensures all characters belong to the character set. More...

Detailed Description

Produce code for simple implementation of String Java libraries.

Definition in file java_string_library_preprocess.h.

Macro Definition Documentation

MAX_FORMAT_ARGS

#define MAX_FORMAT_ARGS   10

Definition at line 32 of file java_string_library_preprocess.h.

Referenced by java_string_library_preprocesst::make_string_format_code().

Function Documentation

add_array_to_length_association()

void add_array_to_length_association	(	const exprt &	array,
		const exprt &	length,
		symbol_table_baset &	symbol_table,
		const source_locationt &	loc,
		code_blockt &	code
	)

Add a call to a primitive of the string solver, letting it know that the actual length of array is length.

Parameters

array	infinite size character array expression
length	integer expression
symbol_table	the symbol table
loc	source location
code	[out] : code block to which declaration and calls get added

Definition at line 718 of file java_string_library_preprocess.cpp.

References code_blockt::add(), code_assign_function_application(), get_fresh_aux_symbol(), java_int_type(), loc, and symbolt::symbol_expr().

Referenced by initialize_nondet_string_fields(), and java_string_library_preprocesst::make_nondet_string_expr().

add_character_set_constraint()

void add_character_set_constraint	(	const exprt &	pointer,
		const exprt &	length,
		const irep_idt &	char_set,
		symbol_table_baset &	symbol_table,
		const source_locationt &	loc,
		code_blockt &	code
	)

Add a call to a primitive of the string solver which ensures all characters belong to the character set.

Parameters

pointer	a character pointer expression
length	length of the character sequence pointed by pointer
char_set	character set given by a range expression consisting of two characters separated by an hyphen. For instance "a-z" denotes all lower case ascii letters.
symbol_table	the symbol table
loc	source location
code	[out] : code block to which declaration and calls get added

Definition at line 753 of file java_string_library_preprocess.cpp.

References code_blockt::add(), code_assign_function_application(), get_fresh_aux_symbol(), irept::id(), java_int_type(), loc, PRECONDITION, and exprt::type().

Referenced by initialize_nondet_string_fields().

add_pointer_to_array_association()

void add_pointer_to_array_association	(	const exprt &	pointer,
		const exprt &	array,
		symbol_table_baset &	symbol_table,
		const source_locationt &	loc,
		code_blockt &	code
	)

Add a call to a primitive of the string solver, letting it know that pointer points to the first character of array.

Parameters

pointer	a character pointer expression
array	a character array expression
symbol_table	the symbol table
loc	source location
code	[out] : code block to which declaration and calls get added

Definition at line 684 of file java_string_library_preprocess.cpp.

References code_blockt::add(), code_assign_function_application(), get_fresh_aux_symbol(), irept::id(), java_int_type(), loc, PRECONDITION, and exprt::type().

Referenced by initialize_nondet_string_fields(), java_string_library_preprocesst::make_nondet_string_expr(), and java_string_library_preprocesst::replace_char_array().

make_nondet_infinite_char_array()

exprt make_nondet_infinite_char_array	(	symbol_table_baset &	symbol_table,
		const source_locationt &	loc,
		const irep_idt &	function_id,
		code_blockt &	code
	)

Declare a fresh symbol of type array of character with infinite size.

Parameters

symbol_table	the symbol table
loc	source location
function_id	name of the function containing the array
code	[out] : code block where the declaration gets added

Returns

created symbol expression

Definition at line 655 of file java_string_library_preprocess.cpp.

References code_blockt::add(), get_fresh_aux_symbol(), id2string(), java_char_type(), java_int_type(), loc, symbolt::symbol_expr(), and exprt::type().

Referenced by initialize_nondet_string_fields(), and java_string_library_preprocesst::make_nondet_string_expr().