cprover
java_utils.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "java_utils.h"
10 
11 #include "java_root_class.h"
13 
14 #include <util/fresh_symbol.h>
15 #include <util/invariant.h>
16 #include <util/mathematical_expr.h>
18 #include <util/message.h>
19 #include <util/prefix.h>
20 #include <util/std_types.h>
21 #include <util/string_utils.h>
22 
23 #include <set>
24 #include <unordered_set>
25 
26 bool java_is_array_type(const typet &type)
27 {
28  if(type.id() != ID_struct)
29  return false;
31 }
32 
33 bool is_java_string_type(const struct_typet &struct_type)
34 {
36  struct_type) &&
37  struct_type.has_component("length") &&
38  struct_type.has_component("data");
39 }
40 
41 bool is_primitive_wrapper_type_name(const std::string &type_name)
42 {
43  static const std::unordered_set<std::string> primitive_wrapper_type_names = {
44  "java.lang.Boolean",
45  "java.lang.Byte",
46  "java.lang.Character",
47  "java.lang.Double",
48  "java.lang.Float",
49  "java.lang.Integer",
50  "java.lang.Long",
51  "java.lang.Short"};
52  return primitive_wrapper_type_names.count(type_name) > 0;
53 }
54 
55 unsigned java_local_variable_slots(const typet &t)
56 {
57 
58  // Even on a 64-bit platform, Java pointers occupy one slot:
59  if(t.id()==ID_pointer)
60  return 1;
61 
62  const std::size_t bitwidth = to_bitvector_type(t).get_width();
63  INVARIANT(
64  bitwidth==8 ||
65  bitwidth==16 ||
66  bitwidth==32 ||
67  bitwidth==64,
68  "all types constructed in java_types.cpp encode JVM types "
69  "with these bit widths");
70 
71  return bitwidth == 64 ? 2u : 1u;
72 }
73 
75 {
76  unsigned slots=0;
77 
78  for(const auto &p : t.parameters())
79  slots+=java_local_variable_slots(p.type());
80 
81  return slots;
82 }
83 
84 const std::string java_class_to_package(const std::string &canonical_classname)
85 {
86  return trim_from_last_delimiter(canonical_classname, '.');
87 }
88 
90  const irep_idt &class_name,
91  symbol_table_baset &symbol_table,
92  message_handlert &message_handler,
93  const struct_union_typet::componentst &componentst)
94 {
95  java_class_typet class_type;
96 
97  class_type.set_tag(class_name);
98  class_type.set_is_stub(true);
99 
100  // produce class symbol
101  symbolt new_symbol;
102  new_symbol.base_name=class_name;
103  new_symbol.pretty_name=class_name;
104  new_symbol.name="java::"+id2string(class_name);
105  class_type.set_name(new_symbol.name);
106  new_symbol.type=class_type;
107  new_symbol.mode=ID_java;
108  new_symbol.is_type=true;
109 
110  std::pair<symbolt &, bool> res=symbol_table.insert(std::move(new_symbol));
111 
112  if(!res.second)
113  {
114  messaget message(message_handler);
115  message.warning() <<
116  "stub class symbol " <<
117  new_symbol.name <<
118  " already exists" << messaget::eom;
119  }
120  else
121  {
122  // create the class identifier etc
123  java_root_class(res.first);
124  java_add_components_to_class(res.first, componentst);
125  }
126 }
127 
129  exprt &expr,
130  const source_locationt &source_location)
131 {
132  expr.add_source_location().merge(source_location);
133  for(exprt &op : expr.operands())
134  merge_source_location_rec(op, source_location);
135 }
136 
138 {
140 }
141 
143  const std::string &friendly_name,
144  const symbol_table_baset &symbol_table,
145  std::string &error)
146 {
147  std::string qualified_name="java::"+friendly_name;
148  if(friendly_name.rfind(':')==std::string::npos)
149  {
150  std::string prefix=qualified_name+':';
151  std::set<irep_idt> matches;
152 
153  for(const auto &s : symbol_table.symbols)
154  if(has_prefix(id2string(s.first), prefix) &&
155  s.second.type.id()==ID_code)
156  matches.insert(s.first);
157 
158  if(matches.empty())
159  {
160  error="'"+friendly_name+"' not found";
161  return irep_idt();
162  }
163  else if(matches.size()>1)
164  {
165  std::ostringstream message;
166  message << "'"+friendly_name+"' is ambiguous between:";
167 
168  // Trim java:: prefix so we can recommend an appropriate input:
169  for(const auto &s : matches)
170  message << "\n " << id2string(s).substr(6);
171 
172  error=message.str();
173  return irep_idt();
174  }
175  else
176  {
177  return *matches.begin();
178  }
179  }
180  else
181  {
182  auto findit=symbol_table.symbols.find(qualified_name);
183  if(findit==symbol_table.symbols.end())
184  {
185  error="'"+friendly_name+"' not found";
186  return irep_idt();
187  }
188  else if(findit->second.type.id()!=ID_code)
189  {
190  error="'"+friendly_name+"' not a function";
191  return irep_idt();
192  }
193  else
194  {
195  return findit->first;
196  }
197  }
198 }
199 
201  const pointer_typet &given_pointer_type,
202  const java_class_typet &replacement_class_type)
203 {
204  if(can_cast_type<struct_tag_typet>(given_pointer_type.subtype()))
205  {
206  struct_tag_typet struct_tag_subtype{replacement_class_type.get_name()};
207  return pointer_type(struct_tag_subtype);
208  }
209  return pointer_type(replacement_class_type);
210 }
211 
213 {
214  dereference_exprt result(expr);
215  // tag it so it's easy to identify during instrumentation
216  result.set(ID_java_member_access, true);
217  return result;
218 }
219 
234  const std::string &src,
235  size_t open_pos,
236  char open_char,
237  char close_char)
238 {
239  // having the same opening and closing delimiter does not allow for hierarchic
240  // structuring
241  PRECONDITION(open_char!=close_char);
242  PRECONDITION(src[open_pos]==open_char);
243  size_t c_pos=open_pos+1;
244  const size_t end_pos=src.size()-1;
245  size_t depth=0;
246 
247  while(c_pos<=end_pos)
248  {
249  if(src[c_pos] == open_char)
250  depth++;
251  else if(src[c_pos] == close_char)
252  {
253  if(depth==0)
254  return c_pos;
255  depth--;
256  }
257  c_pos++;
258  // limit depth to sensible values
259  INVARIANT(
260  depth<=(src.size()-open_pos),
261  "No closing \'"+std::to_string(close_char)+
262  "\' found in signature to parse.");
263  }
264  // did not find corresponding closing '>'
265  return std::string::npos;
266 }
267 
273  symbolt &class_symbol,
274  const struct_union_typet::componentst &components_to_add)
275 {
276  PRECONDITION(class_symbol.is_type);
277  PRECONDITION(class_symbol.type.id()==ID_struct);
278  struct_typet &struct_type=to_struct_type(class_symbol.type);
279  struct_typet::componentst &components=struct_type.components();
280  components.insert(
281  components.end(), components_to_add.begin(), components_to_add.end());
282 }
283 
290  const irep_idt &function_name,
291  const mathematical_function_typet &type,
292  symbol_table_baset &symbol_table)
293 {
294  auxiliary_symbolt func_symbol;
295  func_symbol.base_name=function_name;
296  func_symbol.pretty_name=function_name;
297  func_symbol.is_static_lifetime=false;
298  func_symbol.is_state_var = false;
299  func_symbol.mode=ID_java;
300  func_symbol.name=function_name;
301  func_symbol.type=type;
302  symbol_table.add(func_symbol);
303 
304  return func_symbol;
305 }
306 
316  const irep_idt &function_name,
317  const exprt::operandst &arguments,
318  const typet &range,
319  symbol_table_baset &symbol_table)
320 {
321  std::vector<typet> argument_types;
322  for(const auto &arg : arguments)
323  argument_types.push_back(arg.type());
324 
325  // Declaring the function
326  const auto symbol = declare_function(
327  function_name,
328  mathematical_function_typet(std::move(argument_types), range),
329  symbol_table);
330 
331  // Function application
332  return function_application_exprt(symbol.symbol_expr(), arguments, range);
333 }
334 
339 {
340  const std::string to_strip_str=id2string(to_strip);
341  const std::string prefix="java::";
342 
343  PRECONDITION(has_prefix(to_strip_str, prefix));
344  return to_strip_str.substr(prefix.size(), std::string::npos);
345 }
346 
352 std::string pretty_print_java_type(const std::string &fqn_java_type)
353 {
354  std::string result(fqn_java_type);
355  const std::string java_cbmc_string("java::");
356  // Remove the CBMC internal java identifier
357  if(has_prefix(fqn_java_type, java_cbmc_string))
358  result = fqn_java_type.substr(java_cbmc_string.length());
359  // If the class is in package java.lang strip
360  // package name due to default import
361  const std::string java_lang_string("java.lang.");
362  if(has_prefix(result, java_lang_string))
363  result = result.substr(java_lang_string.length());
364  return result;
365 }
366 
380  const irep_idt &component_class_id,
381  const irep_idt &component_name,
382  const symbol_tablet &symbol_table,
383  bool include_interfaces)
384 {
385  resolve_inherited_componentt component_resolver{symbol_table};
386  const auto resolved_component =
387  component_resolver(component_class_id, component_name, include_interfaces);
388 
389  // resolved_component is a pair (class-name, component-name) found by walking
390  // the chain of class inheritance (not interfaces!) and stopping on the first
391  // class that contains a component of equal name and type to `component_name`
392 
393  if(resolved_component)
394  {
395  // Directly defined on the class referred to?
396  if(component_class_id == resolved_component->get_class_identifier())
397  return *resolved_component;
398 
399  // No, may be inherited from some parent class; check it is visible:
400  const symbolt &component_symbol = symbol_table.lookup_ref(
401  resolved_component->get_full_component_identifier());
402 
403  irep_idt access = component_symbol.type.get(ID_access);
404  if(access.empty())
405  access = component_symbol.type.get(ID_C_access);
406 
407  if(access==ID_public || access==ID_protected)
408  {
409  // since the component is public, it is inherited
410  return *resolved_component;
411  }
412 
413  // components with the default access modifier are only
414  // accessible within the same package.
415  if(access==ID_default)
416  {
417  const std::string &class_package=
418  java_class_to_package(id2string(component_class_id));
419  const std::string &component_package = java_class_to_package(
420  id2string(resolved_component->get_class_identifier()));
421  if(component_package == class_package)
422  return *resolved_component;
423  else
424  return {};
425  }
426 
427  if(access==ID_private)
428  {
429  // We return not-found because the component found by the
430  // component_resolver above proves that `component_name` cannot be
431  // inherited (assuming that the original Java code compiles). This is
432  // because, as we walk the inheritance chain for `classname` from Object
433  // to `classname`, a component can only become "more accessible". So, if
434  // the last occurrence is private, all others before must be private as
435  // well, and none is inherited in `classname`.
436  return {};
437  }
438 
439  UNREACHABLE; // Unexpected access modifier
440  }
441  else
442  {
443  return {};
444  }
445 }
446 
451 {
452  static const irep_idt in = "java::java.lang.System.in";
453  static const irep_idt out = "java::java.lang.System.out";
454  static const irep_idt err = "java::java.lang.System.err";
455  return symbolid == in || symbolid == out || symbolid == err;
456 }
457 
460 const std::unordered_set<std::string> cprover_methods_to_ignore
461 {
462  "nondetBoolean",
463  "nondetByte",
464  "nondetChar",
465  "nondetShort",
466  "nondetInt",
467  "nondetLong",
468  "nondetFloat",
469  "nondetDouble",
470  "nondetWithNull",
471  "nondetWithoutNull",
472  "notModelled",
473  "atomicBegin",
474  "atomicEnd",
475  "startThread",
476  "endThread",
477  "getCurrentThreadID"
478 };
479 
488  const typet &type,
489  const std::string &basename_prefix,
490  const source_locationt &source_location,
491  const irep_idt &function_name,
492  symbol_table_baset &symbol_table)
493 {
494  PRECONDITION(!function_name.empty());
495  const std::string name_prefix = id2string(function_name);
496  return get_fresh_aux_symbol(
497  type, name_prefix, basename_prefix, source_location, ID_java, symbol_table);
498 }
499 
501 {
502  const irep_idt &class_id = symbol.type.get(ID_C_class);
503  return class_id.empty() ? optionalt<irep_idt>{} : class_id;
504 }
505 
507 {
508  symbol.type.set(ID_C_class, declaring_class);
509 }
510 
512 class_name_from_method_name(const std::string &method_name)
513 {
514  const auto signature_index = method_name.rfind(":");
515  const auto method_index = method_name.rfind(".", signature_index);
516  if(method_index == std::string::npos)
517  return {};
518  return method_name.substr(0, method_index);
519 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:152
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:62
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
typet::subtype
const typet & subtype() const
Definition: type.h:47
java_root_class.h
is_primitive_wrapper_type_name
bool is_primitive_wrapper_type_name(const std::string &type_name)
Returns true iff the argument is the fully qualified name of a Java primitive wrapper type.
Definition: java_utils.cpp:41
NODISCARD
#define NODISCARD
Definition: nodiscard.h:22
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
is_java_string_literal_id
bool is_java_string_literal_id(const irep_idt &id)
Definition: java_utils.cpp:137
set_declaring_class
void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class)
Sets the identifier of the class which declared a given symbol to declaring_class.
Definition: java_utils.cpp:506
string_utils.h
typet
The type of an expression, extends irept.
Definition: type.h:29
fresh_symbol.h
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2917
checked_dereference
dereference_exprt checked_dereference(const exprt &expr)
Dereference an expression and flag it for a null-pointer check.
Definition: java_utils.cpp:212
make_function_application
exprt make_function_application(const irep_idt &function_name, const exprt::operandst &arguments, const typet &range, symbol_table_baset &symbol_table)
Create a (mathematical) function application expression.
Definition: java_utils.cpp:315
java_class_to_package
const std::string java_class_to_package(const std::string &canonical_classname)
Definition: java_utils.cpp:84
declaring_class
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
Definition: java_utils.cpp:500
prefix.h
invariant.h
java_is_array_type
bool java_is_array_type(const typet &type)
Definition: java_utils.cpp:26
generate_class_stub
void generate_class_stub(const irep_idt &class_name, symbol_table_baset &symbol_table, message_handlert &message_handler, const struct_union_typet::componentst &componentst)
Definition: java_utils.cpp:89
exprt
Base class for all expressions.
Definition: expr.h:53
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
is_java_array_tag
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:232
java_string_library_preprocess.h
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:490
irep_idt
dstringt irep_idt
Definition: irep.h:32
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:283
auxiliary_symbolt
Internally generated symbol table entry.
Definition: symbol.h:160
trim_from_last_delimiter
std::string trim_from_last_delimiter(const std::string &s, const char delim)
Definition: string_utils.cpp:129
class_name_from_method_name
NODISCARD optionalt< std::string > class_name_from_method_name(const std::string &method_name)
Get JVM type name of the class in which method_name is defined.
Definition: java_utils.cpp:512
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
java_class_typet
Definition: java_types.h:199
mathematical_types.h
strip_java_namespace_prefix
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
Definition: java_utils.cpp:338
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
find_closing_delimiter
size_t find_closing_delimiter(const std::string &src, size_t open_pos, char open_char, char close_char)
Finds the corresponding closing delimiter to the given opening delimiter.
Definition: java_utils.cpp:233
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
is_java_string_type
bool is_java_string_type(const struct_typet &struct_type)
Returns true iff the argument represents a string type (CharSequence, StringBuilder,...
Definition: java_utils.cpp:33
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
struct_union_typet::set_tag
void set_tag(const irep_idt &tag)
Definition: std_types.h:164
can_cast_type< struct_tag_typet >
bool can_cast_type< struct_tag_typet >(const typet &type)
Check whether a reference to a typet is a struct_tag_typet.
Definition: std_types.h:502
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
source_locationt::merge
void merge(const source_locationt &from)
Set all unset source-location fields in this object to their values in 'from'.
Definition: source_location.cpp:73
std_types.h
java_add_components_to_class
void java_add_components_to_class(symbolt &class_symbol, const struct_union_typet::componentst &components_to_add)
Add the components in components_to_add to the class denoted by class symbol.
Definition: java_utils.cpp:272
resolve_friendly_method_name
irep_idt resolve_friendly_method_name(const std::string &friendly_name, const symbol_table_baset &symbol_table, std::string &error)
Resolves a user-friendly method name (like packagename.Class.method) into an internal name (like java...
Definition: java_utils.cpp:142
is_non_null_library_global
bool is_non_null_library_global(const irep_idt &symbolid)
Check if a symbol is a well-known non-null global.
Definition: java_utils.cpp:450
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:191
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
java_string_library_preprocesst::implements_java_char_sequence
static bool implements_java_char_sequence(const typet &type)
Definition: java_string_library_preprocess.h:70
struct_union_typet::has_component
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:152
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:27
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
dstringt::empty
bool empty() const
Definition: dstring.h:88
java_local_variable_slots
unsigned java_local_variable_slots(const typet &t)
Returns the number of JVM local variables (slots) taken by a local variable that, when translated to ...
Definition: java_utils.cpp:55
cprover_methods_to_ignore
const std::unordered_set< std::string > cprover_methods_to_ignore
Methods belonging to the class org.cprover.CProver that should be ignored (not converted),...
Definition: java_utils.cpp:461
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
pointer_to_replacement_type
pointer_typet pointer_to_replacement_type(const pointer_typet &given_pointer_type, const java_class_typet &replacement_class_type)
Given a pointer type to a Java class and a type representing a more specific Java class,...
Definition: java_utils.cpp:200
fresh_java_symbol
symbolt & fresh_java_symbol(const typet &type, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &function_name, symbol_table_baset &symbol_table)
Definition: java_utils.cpp:487
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
get_inherited_component
optionalt< resolve_inherited_componentt::inherited_componentt > get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const symbol_tablet &symbol_table, bool include_interfaces)
Finds an inherited component (method or field), taking component visibility into account.
Definition: java_utils.cpp:379
declare_function
static auxiliary_symbolt declare_function(const irep_idt &function_name, const mathematical_function_typet &type, symbol_table_baset &symbol_table)
Declare a function with the given name and type.
Definition: java_utils.cpp:289
source_locationt
Definition: source_location.h:20
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
java_class_typet::get_name
const irep_idt & get_name() const
Get the name of the struct, which can be used to look up its symbol in the symbol table.
Definition: java_types.h:502
java_class_typet::set_is_stub
void set_is_stub(bool is_stub)
Definition: java_types.h:383
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
merge_source_location_rec
void merge_source_location_rec(exprt &expr, const source_locationt &source_location)
Attaches a source location to an expression and all of its subexpressions.
Definition: java_utils.cpp:128
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
java_method_parameter_slots
unsigned java_method_parameter_slots(const java_method_typet &t)
Returns the the number of JVM local variables (slots) used by the JVM to pass, upon call,...
Definition: java_utils.cpp:74
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
symbolt::is_type
bool is_type
Definition: symbol.h:61
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
java_class_typet::set_name
void set_name(const irep_idt &name)
Set the name of the struct, which can be used to look up its symbol in the symbol table.
Definition: java_types.h:509
symbol_table_baset::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
java_root_class
void java_root_class(symbolt &class_symbol)
Create components to an object of the root class (usually java.lang.Object) Specifically,...
Definition: java_root_class.cpp:22
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
exprt::operands
operandst & operands()
Definition: expr.h:95
pretty_print_java_type
std::string pretty_print_java_type(const std::string &fqn_java_type)
Strip the package name from a java type, for the type to be pretty printed (java::java....
Definition: java_utils.cpp:352
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:257
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
message.h
java_utils.h
java_method_typet
Definition: java_types.h:103
mathematical_function_typet
A type for mathematical functions (do not confuse with functions/methods in code)
Definition: mathematical_types.h:59
get_fresh_aux_symbol
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Definition: fresh_symbol.cpp:32
JAVA_STRING_LITERAL_PREFIX
#define JAVA_STRING_LITERAL_PREFIX
Definition: java_utils.h:68
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089
mathematical_expr.h
resolve_inherited_componentt
Definition: resolve_inherited_component.h:22
get_tag
static irep_idt get_tag(const typet &type)
Definition: java_string_library_preprocess.cpp:37