CBMC
java_string_literals.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Java string literal processing
4 
5 Author: Chris Smowton, chris.smowton@diffblue.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_JAVA_BYTECODE_JAVA_STRING_LITERALS_H
10 #define CPROVER_JAVA_BYTECODE_JAVA_STRING_LITERALS_H
11 
12 #include <util/std_expr.h>
13 
14 class java_string_literal_exprt;
15 class symbol_table_baset;
16 
25 symbol_exprt get_or_create_string_literal_symbol(
26  const java_string_literal_exprt &string_expr,
27  symbol_table_baset &symbol_table,
28  bool string_refinement_enabled);
29 
33 symbol_exprt get_or_create_string_literal_symbol(
34  const irep_idt &string_value,
35  symbol_table_baset &symbol_table,
36  bool string_refinement_enabled);
37 
38 #endif
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
java_string_literal_exprt
Definition: java_string_literal_expr.h:18
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:131
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:23
get_or_create_string_literal_symbol
symbol_exprt get_or_create_string_literal_symbol(const java_string_literal_exprt &string_expr, symbol_table_baset &symbol_table, bool string_refinement_enabled)
Creates or gets an existing constant global symbol for a given string literal.
Definition: java_string_literals.cpp:36
std_expr.h
API to expression classes.