java_string_library_preprocess.h File Reference

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

#include <util/refined_string_type.h>
#include <util/std_code.h>
#include <util/string_expr.h>
#include <goto-programs/goto_instruction_code.h>
#include "character_refine_preprocess.h"
#include "java_types.h"
#include <array>
#include <functional>
#include <unordered_set>

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, const irep_idt &function_id, 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, const irep_idt &function_id, 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_range, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, 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 35 of file java_string_library_preprocess.h.

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,
		const irep_idt &	function_id,
		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
	function_id	name of the function in which the code will be added
[out]	code	code block to which declaration and calls get added

Definition at line 677 of file java_string_library_preprocess.cpp.

add_character_set_constraint()

void add_character_set_constraint	(	const exprt &	pointer,
		const exprt &	length,
		const irep_idt &	char_range,
		symbol_table_baset &	symbol_table,
		const source_locationt &	loc,
		const irep_idt &	function_id,
		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_range	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
	function_id	the name of the function
[out]	code	code block to which declaration and calls get added

Definition at line 709 of file java_string_library_preprocess.cpp.

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,
		const irep_idt &	function_id,
		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
	function_id	name of the function in which the code will be added
[out]	code	code block to which declaration and calls get added

Definition at line 646 of file java_string_library_preprocess.cpp.

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
[out]	code	code block where the declaration gets added

Returns

created symbol expression

Definition at line 614 of file java_string_library_preprocess.cpp.