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 is_java_string_type(const struct_typet &struct_type)
27 {
29  struct_type) &&
30  struct_type.has_component("length") &&
31  struct_type.has_component("data");
32 }
33 
36 {
37  static std::unordered_map<irep_idt, java_boxed_type_infot> type_info_by_name =
38  {
39  {"java::java.lang.Boolean",
40  {"java::java.lang.Boolean.booleanValue:()Z", java_boolean_type()}},
41  {"java::java.lang.Byte",
42  {"java::java.lang.Byte.byteValue:()B", java_byte_type()}},
43  {"java::java.lang.Character",
44  {"java::java.lang.Character.charValue:()C", java_char_type()}},
45  {"java::java.lang.Double",
46  {"java::java.lang.Double.doubleValue:()D", java_double_type()}},
47  {"java::java.lang.Float",
48  {"java::java.lang.Float.floatValue:()F", java_float_type()}},
49  {"java::java.lang.Integer",
50  {"java::java.lang.Integer.intValue:()I", java_int_type()}},
51  {"java::java.lang.Long",
52  {"java::java.lang.Long.longValue:()J", java_long_type()}},
53  {"java::java.lang.Short",
54  {"java::java.lang.Short.shortValue:()S", java_short_type()}},
55  };
56 
57  auto found = type_info_by_name.find(type_name);
58  return found == type_info_by_name.end() ? nullptr : &found->second;
59 }
60 
62 get_java_primitive_type_info(const typet &maybe_primitive_type)
63 {
64  static std::unordered_map<typet, java_primitive_type_infot, irep_hash>
65  type_info_by_primitive_type = {
67  {"java::java.lang.Boolean",
68  "java::java.lang.Boolean.valueOf:(Z)Ljava/lang/Boolean;",
69  "java::java.lang.Boolean.booleanValue:()Z"}},
70  {java_byte_type(),
71  {"java::java.lang.Byte",
72  "java::java.lang.Byte.valueOf:(B)Ljava/lang/Byte;",
73  "java::java.lang.Number.byteValue:()B"}},
74  {java_char_type(),
75  {"java::java.lang.Character",
76  "java::java.lang.Character.valueOf:(C)"
77  "Ljava/lang/Character;",
78  "java::java.lang.Character.charValue:()C"}},
80  {"java::java.lang.Double",
81  "java::java.lang.Double.valueOf:(D)"
82  "Ljava/lang/Double;",
83  "java::java.lang.Number.doubleValue:()D"}},
84  {java_float_type(),
85  {"java::java.lang.Float",
86  "java::java.lang.Float.valueOf:(F)"
87  "Ljava/lang/Float;",
88  "java::java.lang.Number.floatValue:()F"}},
89  {java_int_type(),
90  {"java::java.lang.Integer",
91  "java::java.lang.Integer.valueOf:(I)"
92  "Ljava/lang/Integer;",
93  "java::java.lang.Number.intValue:()I"}},
94  {java_long_type(),
95  {"java::java.lang.Long",
96  "java::java.lang.Long.valueOf:(J)Ljava/lang/Long;",
97  "java::java.lang.Number.longValue:()J"}},
98  {java_short_type(),
99  {"java::java.lang.Short",
100  "java::java.lang.Short.valueOf:(S)"
101  "Ljava/lang/Short;",
102  "java::java.lang.Number.shortValue:()S"}}};
103 
104  auto found = type_info_by_primitive_type.find(maybe_primitive_type);
105  return found == type_info_by_primitive_type.end() ? nullptr : &found->second;
106 }
107 
109 {
110  return get_boxed_type_info_by_name(id) != nullptr;
111 }
112 
113 bool is_primitive_wrapper_type_name(const std::string &type_name)
114 {
115  static const std::unordered_set<std::string> primitive_wrapper_type_names = {
116  "java.lang.Boolean",
117  "java.lang.Byte",
118  "java.lang.Character",
119  "java.lang.Double",
120  "java.lang.Float",
121  "java.lang.Integer",
122  "java.lang.Long",
123  "java.lang.Short"};
124  return primitive_wrapper_type_names.count(type_name) > 0;
125 }
126 
128 {
129 
130  // Even on a 64-bit platform, Java pointers occupy one slot:
131  if(t.id()==ID_pointer)
132  return 1;
133 
134  const std::size_t bitwidth = to_bitvector_type(t).get_width();
135  INVARIANT(
136  bitwidth==8 ||
137  bitwidth==16 ||
138  bitwidth==32 ||
139  bitwidth==64,
140  "all types constructed in java_types.cpp encode JVM types "
141  "with these bit widths");
142 
143  return bitwidth == 64 ? 2u : 1u;
144 }
145 
147 {
148  unsigned slots=0;
149 
150  for(const auto &p : t.parameters())
151  slots+=java_local_variable_slots(p.type());
152 
153  return slots;
154 }
155 
156 const std::string java_class_to_package(const std::string &canonical_classname)
157 {
158  return trim_from_last_delimiter(canonical_classname, '.');
159 }
160 
162  const irep_idt &class_name,
163  symbol_table_baset &symbol_table,
164  message_handlert &message_handler,
165  const struct_union_typet::componentst &componentst)
166 {
167  java_class_typet class_type;
168 
169  class_type.set_tag(class_name);
170  class_type.set_is_stub(true);
171 
172  // produce class symbol
173  symbolt new_symbol;
174  new_symbol.base_name=class_name;
175  new_symbol.pretty_name=class_name;
176  new_symbol.name="java::"+id2string(class_name);
177  class_type.set_name(new_symbol.name);
178  new_symbol.type=class_type;
179  new_symbol.mode=ID_java;
180  new_symbol.is_type=true;
181 
182  std::pair<symbolt &, bool> res=symbol_table.insert(std::move(new_symbol));
183 
184  if(!res.second)
185  {
186  messaget message(message_handler);
187  message.warning() <<
188  "stub class symbol " <<
189  new_symbol.name <<
190  " already exists" << messaget::eom;
191  }
192  else
193  {
194  // create the class identifier etc
195  java_root_class(res.first);
196  java_add_components_to_class(res.first, componentst);
197  }
198 }
199 
201  exprt &expr,
202  const source_locationt &source_location)
203 {
204  expr.add_source_location().merge(source_location);
205  for(exprt &op : expr.operands())
206  merge_source_location_rec(op, source_location);
207 }
208 
210 {
212 }
213 
215  const std::string &friendly_name,
216  const symbol_table_baset &symbol_table,
217  std::string &error)
218 {
219  std::string qualified_name="java::"+friendly_name;
220  if(friendly_name.rfind(':')==std::string::npos)
221  {
222  std::string prefix=qualified_name+':';
223  std::set<irep_idt> matches;
224 
225  for(const auto &s : symbol_table.symbols)
226  if(has_prefix(id2string(s.first), prefix) &&
227  s.second.type.id()==ID_code)
228  matches.insert(s.first);
229 
230  if(matches.empty())
231  {
232  error="'"+friendly_name+"' not found";
233  return irep_idt();
234  }
235  else if(matches.size()>1)
236  {
237  std::ostringstream message;
238  message << "'"+friendly_name+"' is ambiguous between:";
239 
240  // Trim java:: prefix so we can recommend an appropriate input:
241  for(const auto &s : matches)
242  message << "\n " << id2string(s).substr(6);
243 
244  error=message.str();
245  return irep_idt();
246  }
247  else
248  {
249  return *matches.begin();
250  }
251  }
252  else
253  {
254  auto findit=symbol_table.symbols.find(qualified_name);
255  if(findit==symbol_table.symbols.end())
256  {
257  error="'"+friendly_name+"' not found";
258  return irep_idt();
259  }
260  else if(findit->second.type.id()!=ID_code)
261  {
262  error="'"+friendly_name+"' not a function";
263  return irep_idt();
264  }
265  else
266  {
267  return findit->first;
268  }
269  }
270 }
271 
273  const pointer_typet &given_pointer_type,
274  const java_class_typet &replacement_class_type)
275 {
276  if(can_cast_type<struct_tag_typet>(given_pointer_type.base_type()))
277  {
278  struct_tag_typet struct_tag_subtype{replacement_class_type.get_name()};
279  return pointer_type(struct_tag_subtype);
280  }
281  return pointer_type(replacement_class_type);
282 }
283 
285 {
286  dereference_exprt result(expr);
287  // tag it so it's easy to identify during instrumentation
288  result.set(ID_java_member_access, true);
289  return result;
290 }
291 
306  const std::string &src,
307  size_t open_pos,
308  char open_char,
309  char close_char)
310 {
311  // having the same opening and closing delimiter does not allow for hierarchic
312  // structuring
313  PRECONDITION(open_char!=close_char);
314  PRECONDITION(src[open_pos]==open_char);
315  size_t c_pos=open_pos+1;
316  const size_t end_pos=src.size()-1;
317  size_t depth=0;
318 
319  while(c_pos<=end_pos)
320  {
321  if(src[c_pos] == open_char)
322  depth++;
323  else if(src[c_pos] == close_char)
324  {
325  if(depth==0)
326  return c_pos;
327  depth--;
328  }
329  c_pos++;
330  // limit depth to sensible values
331  INVARIANT(
332  depth<=(src.size()-open_pos),
333  "No closing \'"+std::to_string(close_char)+
334  "\' found in signature to parse.");
335  }
336  // did not find corresponding closing '>'
337  return std::string::npos;
338 }
339 
345  symbolt &class_symbol,
346  const struct_union_typet::componentst &components_to_add)
347 {
348  PRECONDITION(class_symbol.is_type);
349  PRECONDITION(class_symbol.type.id()==ID_struct);
350  struct_typet &struct_type=to_struct_type(class_symbol.type);
351  struct_typet::componentst &components=struct_type.components();
352  components.insert(
353  components.end(), components_to_add.begin(), components_to_add.end());
354 }
355 
362  const irep_idt &function_name,
363  const mathematical_function_typet &type,
364  symbol_table_baset &symbol_table)
365 {
366  auxiliary_symbolt func_symbol;
367  func_symbol.base_name=function_name;
368  func_symbol.pretty_name=function_name;
369  func_symbol.is_static_lifetime=false;
370  func_symbol.is_state_var = false;
371  func_symbol.mode=ID_java;
372  func_symbol.name=function_name;
373  func_symbol.type=type;
374  symbol_table.add(func_symbol);
375 
376  return func_symbol;
377 }
378 
388  const irep_idt &function_name,
389  const exprt::operandst &arguments,
390  const typet &range,
391  symbol_table_baset &symbol_table)
392 {
393  std::vector<typet> argument_types;
394  for(const auto &arg : arguments)
395  argument_types.push_back(arg.type());
396 
397  // Declaring the function
398  const auto symbol = declare_function(
399  function_name,
400  mathematical_function_typet(std::move(argument_types), range),
401  symbol_table);
402 
403  // Function application
404  return function_application_exprt{symbol.symbol_expr(), arguments};
405 }
406 
411 {
412  const std::string to_strip_str=id2string(to_strip);
413  const std::string prefix="java::";
414 
415  PRECONDITION(has_prefix(to_strip_str, prefix));
416  return to_strip_str.substr(prefix.size(), std::string::npos);
417 }
418 
424 std::string pretty_print_java_type(const std::string &fqn_java_type)
425 {
426  std::string result(fqn_java_type);
427  const std::string java_cbmc_string("java::");
428  // Remove the CBMC internal java identifier
429  if(has_prefix(fqn_java_type, java_cbmc_string))
430  result = fqn_java_type.substr(java_cbmc_string.length());
431  // If the class is in package java.lang strip
432  // package name due to default import
433  const std::string java_lang_string("java.lang.");
434  if(has_prefix(result, java_lang_string))
435  result = result.substr(java_lang_string.length());
436  return result;
437 }
438 
452  const irep_idt &component_class_id,
453  const irep_idt &component_name,
454  const symbol_tablet &symbol_table,
455  bool include_interfaces)
456 {
457  resolve_inherited_componentt component_resolver{symbol_table};
458  const auto resolved_component =
459  component_resolver(component_class_id, component_name, include_interfaces);
460 
461  // resolved_component is a pair (class-name, component-name) found by walking
462  // the chain of class inheritance (not interfaces!) and stopping on the first
463  // class that contains a component of equal name and type to `component_name`
464 
465  if(resolved_component)
466  {
467  // Directly defined on the class referred to?
468  if(component_class_id == resolved_component->get_class_identifier())
469  return *resolved_component;
470 
471  // No, may be inherited from some parent class; check it is visible:
472  const symbolt &component_symbol = symbol_table.lookup_ref(
473  resolved_component->get_full_component_identifier());
474 
475  irep_idt access = component_symbol.type.get(ID_access);
476  if(access.empty())
477  access = component_symbol.type.get(ID_C_access);
478 
479  if(access==ID_public || access==ID_protected)
480  {
481  // since the component is public, it is inherited
482  return *resolved_component;
483  }
484 
485  // components with the default access modifier are only
486  // accessible within the same package.
487  if(access==ID_default)
488  {
489  const std::string &class_package=
490  java_class_to_package(id2string(component_class_id));
491  const std::string &component_package = java_class_to_package(
492  id2string(resolved_component->get_class_identifier()));
493  if(component_package == class_package)
494  return *resolved_component;
495  else
496  return {};
497  }
498 
499  if(access==ID_private)
500  {
501  // We return not-found because the component found by the
502  // component_resolver above proves that `component_name` cannot be
503  // inherited (assuming that the original Java code compiles). This is
504  // because, as we walk the inheritance chain for `classname` from Object
505  // to `classname`, a component can only become "more accessible". So, if
506  // the last occurrence is private, all others before must be private as
507  // well, and none is inherited in `classname`.
508  return {};
509  }
510 
511  UNREACHABLE; // Unexpected access modifier
512  }
513  else
514  {
515  return {};
516  }
517 }
518 
523 {
524  static const irep_idt in = "java::java.lang.System.in";
525  static const irep_idt out = "java::java.lang.System.out";
526  static const irep_idt err = "java::java.lang.System.err";
527  return symbolid == in || symbolid == out || symbolid == err;
528 }
529 
532 const std::unordered_set<std::string> cprover_methods_to_ignore{
533  "nondetBoolean",
534  "nondetByte",
535  "nondetChar",
536  "nondetShort",
537  "nondetInt",
538  "nondetLong",
539  "nondetFloat",
540  "nondetDouble",
541  "nondetWithNull",
542  "nondetWithoutNull",
543  "notModelled",
544  "atomicBegin",
545  "atomicEnd",
546  "startThread",
547  "endThread",
548  "getCurrentThreadId",
549  "getMonitorCount"};
550 
559  const typet &type,
560  const std::string &basename_prefix,
561  const source_locationt &source_location,
562  const irep_idt &function_name,
563  symbol_table_baset &symbol_table)
564 {
565  PRECONDITION(!function_name.empty());
566  const std::string name_prefix = id2string(function_name);
567  return get_fresh_aux_symbol(
568  type, name_prefix, basename_prefix, source_location, ID_java, symbol_table);
569 }
570 
572 {
573  const irep_idt &class_id = symbol.type.get(ID_C_class);
574  return class_id.empty() ? optionalt<irep_idt>{} : class_id;
575 }
576 
578 {
579  symbol.type.set(ID_C_class, declaring_class);
580 }
581 
583 class_name_from_method_name(const std::string &method_name)
584 {
585  const auto signature_index = method_name.rfind(":");
586  const auto method_index = method_name.rfind(".", signature_index);
587  if(method_index == std::string::npos)
588  return {};
589  return method_name.substr(0, method_index);
590 }
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:147
std::size_t get_width() const
Definition: std_types.h:864
const parameterst & parameters() const
Definition: std_types.h:655
Operator to dereference a pointer.
Definition: pointer_expr.h:648
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
source_locationt & add_source_location()
Definition: expr.h:235
operandst & operands()
Definition: expr.h:92
Application of (mathematical) function.
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
const irep_idt & id() const
Definition: irep.h:396
void set_is_stub(bool is_stub)
Definition: java_types.h:393
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:564
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:557
static bool implements_java_char_sequence(const typet &type)
A type for mathematical functions (do not confuse with functions/methods in code)
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & warning() const
Definition: message.h:404
static eomt eom
Definition: message.h:297
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
void merge(const source_locationt &from)
Set all unset source-location fields in this object to their values in 'from'.
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:449
Structure type, corresponds to C style structs.
Definition: std_types.h:231
void set_tag(const irep_idt &tag)
Definition: std_types.h:169
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:157
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
The symbol table base class interface.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_static_lifetime
Definition: symbol.h:65
bool is_type
Definition: symbol.h:61
bool is_state_var
Definition: symbol.h:62
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
irep_idt mode
Language mode.
Definition: symbol.h:49
The type of an expression, extends irept.
Definition: type.h:29
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
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 ...
Fresh auxiliary symbol creation.
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
void java_root_class(symbolt &class_symbol)
Create components to an object of the root class (usually java.lang.Object) Specifically,...
Produce code for simple implementation of String Java libraries.
signedbv_typet java_int_type()
Definition: java_types.cpp:31
signedbv_typet java_byte_type()
Definition: java_types.cpp:55
signedbv_typet java_short_type()
Definition: java_types.cpp:49
floatbv_typet java_double_type()
Definition: java_types.cpp:73
floatbv_typet java_float_type()
Definition: java_types.cpp:67
c_bool_typet java_boolean_type()
Definition: java_types.cpp:79
unsignedbv_typet java_char_type()
Definition: java_types.cpp:61
signedbv_typet java_long_type()
Definition: java_types.cpp:43
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 (for examp...
Definition: java_utils.cpp:113
bool is_java_string_literal_id(const irep_idt &id)
Definition: java_utils.cpp:209
const java_primitive_type_infot * get_java_primitive_type_info(const typet &maybe_primitive_type)
If primitive_type is a Java primitive type, return information about it, otherwise return null.
Definition: java_utils.cpp:62
const java_boxed_type_infot * get_boxed_type_info_by_name(const irep_idt &type_name)
If type_name is a Java boxed type tag, return information about it, otherwise return null.
Definition: java_utils.cpp:35
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:344
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:532
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:522
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:451
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:558
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:214
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
Definition: java_utils.cpp:571
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:361
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:577
bool is_primitive_wrapper_type_id(const irep_idt &id)
Returns true iff the argument is the symbol-table identifier of a Java primitive wrapper type (for ex...
Definition: java_utils.cpp:108
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:161
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:26
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:146
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:305
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
Definition: java_utils.cpp:410
dereference_exprt checked_dereference(const exprt &expr)
Dereference an expression and flag it for a null-pointer check.
Definition: java_utils.cpp:284
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:387
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:272
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:127
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:583
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:200
const std::string java_class_to_package(const std::string &canonical_classname)
Definition: java_utils.cpp:156
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:424
#define JAVA_STRING_LITERAL_PREFIX
Definition: java_utils.h:104
API to expression classes for 'mathematical' expressions.
Mathematical types.
#define NODISCARD
Definition: nodiscard.h:22
nonstd::optional< T > optionalt
Definition: optional.h:35
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
Pre-defined types.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
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:461
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::string trim_from_last_delimiter(const std::string &s, const char delim)
Return type for get_boxed_type_info_by_name.
Definition: java_utils.h:54
Return type for get_java_primitive_type_info.
Definition: java_utils.h:34