cprover
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

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
arrayinfinite size character array expression
lengthinteger expression
symbol_tablethe symbol table
locsource 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
pointera character pointer expression
lengthlength of the character sequence pointed by pointer
char_setcharacter 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_tablethe symbol table
locsource 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
pointera character pointer expression
arraya character array expression
symbol_tablethe symbol table
locsource 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_tablethe symbol table
locsource location
function_idname 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().