Loading...

Searching...

No Matches

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.

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.

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.

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.

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 678 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 710 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 647 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 615 of file java_string_library_preprocess.cpp.