CBMC: /home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_utils.cpp Source File

27 bool is_java_string_type(const struct_typet &struct_type)

28{

29 return java_string_library_preprocesst::implements_java_char_sequence(

30 struct_type) &&

31 struct_type.has_component("length") &&

32 struct_type.has_component("data");

33}

36 get_boxed_type_info_by_name(const irep_idt &type_name)

37{

38 static std::unordered_map<irep_idt, java_boxed_type_infot> type_info_by_name =

39 {

40 {"java::java.lang.Boolean",

41 {"java::java.lang.Boolean.booleanValue:()Z", java_boolean_type()}},

42 {"java::java.lang.Byte",

43 {"java::java.lang.Byte.byteValue:()B", java_byte_type()}},

44 {"java::java.lang.Character",

45 {"java::java.lang.Character.charValue:()C", java_char_type()}},

46 {"java::java.lang.Double",

47 {"java::java.lang.Double.doubleValue:()D", java_double_type()}},

48 {"java::java.lang.Float",

49 {"java::java.lang.Float.floatValue:()F", java_float_type()}},

50 {"java::java.lang.Integer",

51 {"java::java.lang.Integer.intValue:()I", java_int_type()}},

52 {"java::java.lang.Long",

53 {"java::java.lang.Long.longValue:()J", java_long_type()}},

54 {"java::java.lang.Short",

55 {"java::java.lang.Short.shortValue:()S", java_short_type()}},

56 };

57

58 auto found = type_info_by_name.find(type_name);

59 return found == type_info_by_name.end() ? nullptr : &found->second;

60}

63 get_java_primitive_type_info(const typet &maybe_primitive_type)

64{

65 static std::unordered_map<typet, java_primitive_type_infot, irep_hash>

66 type_info_by_primitive_type = {

67 {java_boolean_type(),

68 {"java::java.lang.Boolean",

69 "java::java.lang.Boolean.valueOf:(Z)Ljava/lang/Boolean;",

70 "java::java.lang.Boolean.booleanValue:()Z"}},

71 {java_byte_type(),

72 {"java::java.lang.Byte",

73 "java::java.lang.Byte.valueOf:(B)Ljava/lang/Byte;",

74 "java::java.lang.Number.byteValue:()B"}},

75 {java_char_type(),

76 {"java::java.lang.Character",

77 "java::java.lang.Character.valueOf:(C)"

78 "Ljava/lang/Character;",

79 "java::java.lang.Character.charValue:()C"}},

80 {java_double_type(),

81 {"java::java.lang.Double",

82 "java::java.lang.Double.valueOf:(D)"

83 "Ljava/lang/Double;",

84 "java::java.lang.Number.doubleValue:()D"}},

85 {java_float_type(),

86 {"java::java.lang.Float",

87 "java::java.lang.Float.valueOf:(F)"

88 "Ljava/lang/Float;",

89 "java::java.lang.Number.floatValue:()F"}},

90 {java_int_type(),

91 {"java::java.lang.Integer",

92 "java::java.lang.Integer.valueOf:(I)"

93 "Ljava/lang/Integer;",

94 "java::java.lang.Number.intValue:()I"}},

95 {java_long_type(),

96 {"java::java.lang.Long",

97 "java::java.lang.Long.valueOf:(J)Ljava/lang/Long;",

98 "java::java.lang.Number.longValue:()J"}},

99 {java_short_type(),

100 {"java::java.lang.Short",

101 "java::java.lang.Short.valueOf:(S)"

102 "Ljava/lang/Short;",

103 "java::java.lang.Number.shortValue:()S"}}};

104

105 auto found = type_info_by_primitive_type.find(maybe_primitive_type);

106 return found == type_info_by_primitive_type.end() ? nullptr : &found->second;

107}

109 bool is_primitive_wrapper_type_id(const irep_idt &id)

110{

111 return get_boxed_type_info_by_name(id) != nullptr;

112}

114 bool is_primitive_wrapper_type_name(const std::string &type_name)

115{

116 static const std::unordered_set<std::string> primitive_wrapper_type_names = {

117 "java.lang.Boolean",

118 "java.lang.Byte",

119 "java.lang.Character",

120 "java.lang.Double",

121 "java.lang.Float",

122 "java.lang.Integer",

123 "java.lang.Long",

124 "java.lang.Short"};

125 return primitive_wrapper_type_names.count(type_name) > 0;

126}

128 unsigned java_local_variable_slots(const typet &t)

129{

130

131 // Even on a 64-bit platform, Java pointers occupy one slot:

132 if(t.id()==ID_pointer)

133 return 1;

134

135 const std::size_t bitwidth = to_bitvector_type(t).get_width();

136 INVARIANT(

137 bitwidth==8 ||

138 bitwidth==16 ||

139 bitwidth==32 ||

140 bitwidth==64,

141 "all types constructed in java_types.cpp encode JVM types "

142 "with these bit widths");

143

144 return bitwidth == 64 ? 2u : 1u;

145}

147 unsigned java_method_parameter_slots(const java_method_typet &t)

148{

149 unsigned slots=0;

150

151 for(const auto &p : t.parameters())

152 slots+=java_local_variable_slots(p.type());

153

154 return slots;

155}

157 const std::string java_class_to_package(const std::string &canonical_classname)

158{

159 return trim_from_last_delimiter(canonical_classname, '.');

160}

162 void generate_class_stub(

163 const irep_idt &class_name,

164 symbol_table_baset &symbol_table,

165 message_handlert &message_handler,

166 const struct_union_typet::componentst &componentst)

167{

168 java_class_typet class_type;

169

170 class_type.set_tag(class_name);

171 class_type.set_is_stub(true);

172

173 // produce class symbol

174 irep_idt qualified_class_name = "java::" + id2string(class_name);

175 class_type.set_name(qualified_class_name);

176 type_symbolt new_symbol{qualified_class_name, std::move(class_type), ID_java};

177 new_symbol.base_name=class_name;

178 new_symbol.pretty_name=class_name;

179

180 std::pair<symbolt &, bool> res=symbol_table.insert(std::move(new_symbol));

181

182 if(!res.second)

183 {

184 messaget message(message_handler);

185 message.warning() <<

186 "stub class symbol " <<

187 new_symbol.name <<

188 " already exists" << messaget::eom;

189 }

190 else

191 {

192 // create the class identifier etc

193 java_root_class(res.first);

194 java_add_components_to_class(res.first, componentst);

195 }

196}

198 void merge_source_location_rec(

199 exprt &expr,

200 const source_locationt &source_location)

201{

202 expr.add_source_location().merge(source_location);

203 for(exprt &op : expr.operands())

204 merge_source_location_rec(op, source_location);

205}

207 bool is_java_string_literal_id(const irep_idt &id)

208{

209 return id.starts_with(JAVA_STRING_LITERAL_PREFIX);

210}

212 irep_idt resolve_friendly_method_name(

213 const std::string &friendly_name,

214 const symbol_table_baset &symbol_table,

215 std::string &error)

216{

217 std::string qualified_name="java::"+friendly_name;

218 if(friendly_name.rfind(':')==std::string::npos)

219 {

220 std::string prefix=qualified_name+':';

221 std::set<irep_idt> matches;

222

223 for(const auto &s : symbol_table.symbols)

224 if(s.first.starts_with(prefix) && s.second.type.id() == ID_code)

225 matches.insert(s.first);

226

227 if(matches.empty())

228 {

229 error="'"+friendly_name+"' not found";

230 return irep_idt();

231 }

232 else if(matches.size()>1)

233 {

234 std::ostringstream message;

235 message << "'"+friendly_name+"' is ambiguous between:";

236

237 // Trim java:: prefix so we can recommend an appropriate input:

238 for(const auto &s : matches)

239 message << "\n " << id2string(s).substr(6);

240

241 error=message.str();

242 return irep_idt();

243 }

244 else

245 {

246 return *matches.begin();

247 }

248 }

249 else

250 {

251 auto findit=symbol_table.symbols.find(qualified_name);

252 if(findit==symbol_table.symbols.end())

253 {

254 error="'"+friendly_name+"' not found";

255 return irep_idt();

256 }

257 else if(findit->second.type.id()!=ID_code)

258 {

259 error="'"+friendly_name+"' not a function";

260 return irep_idt();

261 }

262 else

263 {

264 return findit->first;

265 }

266 }

267}

269 pointer_typet pointer_to_replacement_type(

270 const pointer_typet &given_pointer_type,

271 const java_class_typet &replacement_class_type)

272{

273 if(can_cast_type<struct_tag_typet>(given_pointer_type.base_type()))

274 {

275 struct_tag_typet struct_tag_subtype{replacement_class_type.get_name()};

276 return pointer_type(struct_tag_subtype);

277 }

278 return pointer_type(replacement_class_type);

279}

281 dereference_exprt checked_dereference(const exprt &expr)

282{

283 dereference_exprt result(expr);

284 // tag it so it's easy to identify during instrumentation

285 result.set(ID_java_member_access, true);

286 return result;

287}

302 size_t find_closing_delimiter(

303 const std::string &src,

304 size_t open_pos,

305 char open_char,

306 char close_char)

307{

308 // having the same opening and closing delimiter does not allow for hierarchic

309 // structuring

310 PRECONDITION(open_char!=close_char);

311 PRECONDITION(src[open_pos]==open_char);

312 size_t c_pos=open_pos+1;

313 const size_t end_pos=src.size()-1;

314 size_t depth=0;

315

316 while(c_pos<=end_pos)

317 {

318 if(src[c_pos] == open_char)

319 depth++;

320 else if(src[c_pos] == close_char)

321 {

322 if(depth==0)

323 return c_pos;

324 depth--;

325 }

326 c_pos++;

327 // limit depth to sensible values

328 INVARIANT(

329 depth<=(src.size()-open_pos),

330 "No closing \'"+std::to_string(close_char)+

331 "\' found in signature to parse.");

332 }

333 // did not find corresponding closing '>'

334 return std::string::npos;

335}

341 void java_add_components_to_class(

342 symbolt &class_symbol,

343 const struct_union_typet::componentst &components_to_add)

344{

345 PRECONDITION(class_symbol.is_type);

346 PRECONDITION(class_symbol.type.id()==ID_struct);

347 struct_typet &struct_type=to_struct_type(class_symbol.type);

348 struct_typet::componentst &components=struct_type.components();

349 components.insert(

350 components.end(), components_to_add.begin(), components_to_add.end());

351}

358 static auxiliary_symbolt declare_function(

359 const irep_idt &function_name,

360 const mathematical_function_typet &type,

361 symbol_table_baset &symbol_table)

362{

363 auxiliary_symbolt func_symbol;

364 func_symbol.base_name=function_name;

365 func_symbol.pretty_name=function_name;

366 func_symbol.is_static_lifetime=false;

367 func_symbol.is_state_var = false;

368 func_symbol.mode=ID_java;

369 func_symbol.name=function_name;

370 func_symbol.type=type;

371 symbol_table.add(func_symbol);

372

373 return func_symbol;

374}

384 exprt make_function_application(

385 const irep_idt &function_name,

386 const exprt::operandst &arguments,

387 const typet &range,

388 symbol_table_baset &symbol_table)

389{

390 std::vector<typet> argument_types;

391 for(const auto &arg : arguments)

392 argument_types.push_back(arg.type());

393

394 // Declaring the function

395 const auto symbol = declare_function(

396 function_name,

397 mathematical_function_typet(std::move(argument_types), range),

398 symbol_table);

399

400 // Function application

401 return function_application_exprt{symbol.symbol_expr(), arguments};

402}

407 irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)

408{

409 const std::string to_strip_str=id2string(to_strip);

410 const std::string prefix="java::";

411

412 PRECONDITION(has_prefix(to_strip_str, prefix));

413 return to_strip_str.substr(prefix.size(), std::string::npos);

414}

421 std::string pretty_print_java_type(const std::string &fqn_java_type)

422{

423 std::string result(fqn_java_type);

424 const std::string java_cbmc_string("java::");

425 // Remove the CBMC internal java identifier

426 if(has_prefix(fqn_java_type, java_cbmc_string))

427 result = fqn_java_type.substr(java_cbmc_string.length());

428 // If the class is in package java.lang strip

429 // package name due to default import

430 const std::string java_lang_string("java.lang.");

431 if(has_prefix(result, java_lang_string))

432 result = result.substr(java_lang_string.length());

433 return result;

434}

448 get_inherited_component(

449 const irep_idt &component_class_id,

450 const irep_idt &component_name,

451 const symbol_table_baset &symbol_table,

452 bool include_interfaces)

453{

454 resolve_inherited_componentt component_resolver{symbol_table};

455 const auto resolved_component =

456 component_resolver(component_class_id, component_name, include_interfaces);

457

458 // resolved_component is a pair (class-name, component-name) found by walking

459 // the chain of class inheritance (not interfaces!) and stopping on the first

460 // class that contains a component of equal name and type to `component_name`

461

462 if(resolved_component)

463 {

464 // Directly defined on the class referred to?

465 if(component_class_id == resolved_component->get_class_identifier())

466 return *resolved_component;

467

468 // No, may be inherited from some parent class; check it is visible:

469 const symbolt &component_symbol = symbol_table.lookup_ref(

470 resolved_component->get_full_component_identifier());

471

472 irep_idt access = component_symbol.type.get(ID_access);

473 if(access.empty())

474 access = component_symbol.type.get(ID_C_access);

475

476 if(access==ID_public || access==ID_protected)

477 {

478 // since the component is public, it is inherited

479 return *resolved_component;

480 }

481

482 // components with the default access modifier are only

483 // accessible within the same package.

484 if(access==ID_default)

485 {

486 const std::string &class_package=

487 java_class_to_package(id2string(component_class_id));

488 const std::string &component_package = java_class_to_package(

489 id2string(resolved_component->get_class_identifier()));

490 if(component_package == class_package)

491 return *resolved_component;

492 else

493 return {};

494 }

495

496 if(access==ID_private)

497 {

498 // We return not-found because the component found by the

499 // component_resolver above proves that `component_name` cannot be

500 // inherited (assuming that the original Java code compiles). This is

501 // because, as we walk the inheritance chain for `classname` from Object

502 // to `classname`, a component can only become "more accessible". So, if

503 // the last occurrence is private, all others before must be private as

504 // well, and none is inherited in `classname`.

505 return {};

506 }

507

508 UNREACHABLE; // Unexpected access modifier

509 }

510 else

511 {

512 return {};

513 }

514}

519 bool is_non_null_library_global(const irep_idt &symbolid)

520{

521 static const irep_idt in = "java::java.lang.System.in";

522 static const irep_idt out = "java::java.lang.System.out";

523 static const irep_idt err = "java::java.lang.System.err";

524 return symbolid == in || symbolid == out || symbolid == err;

525}

529 const std::unordered_set<std::string> cprover_methods_to_ignore{

530 "nondetBoolean",

531 "nondetByte",

532 "nondetChar",

533 "nondetShort",

534 "nondetInt",

535 "nondetLong",

536 "nondetFloat",

537 "nondetDouble",

538 "nondetWithNull",

539 "nondetWithoutNull",

540 "notModelled",

541 "atomicBegin",

542 "atomicEnd",

543 "startThread",

544 "endThread",

545 "getCurrentThreadId",

546 "getMonitorCount"};

555 symbolt &fresh_java_symbol(

556 const typet &type,

557 const std::string &basename_prefix,

558 const source_locationt &source_location,

559 const irep_idt &function_name,

560 symbol_table_baset &symbol_table)

561{

562 PRECONDITION(!function_name.empty());

563 const std::string name_prefix = id2string(function_name);

564 return get_fresh_aux_symbol(

565 type, name_prefix, basename_prefix, source_location, ID_java, symbol_table);

566}

568 std::optional<irep_idt> declaring_class(const symbolt &symbol)

569{

570 const irep_idt &class_id = symbol.type.get(ID_C_class);

571 return class_id.empty() ? std::optional<irep_idt>{} : class_id;

572}

574 void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class)

575{

576 symbol.type.set(ID_C_class, declaring_class);

577}

580 class_name_from_method_name(const std::string &method_name)

581{

582 const auto signature_index = method_name.rfind(":");

583 const auto method_index = method_name.rfind(".", signature_index);

584 if(method_index == std::string::npos)

585 return {};

586 return method_name.substr(0, method_index);

587}

to_bitvector_type

const bitvector_typet & to_bitvector_type(const typet &type)

Cast a typet to a bitvector_typet.

Definition bitvector_types.h:99

pointer_type

pointer_typet pointer_type(const typet &subtype)

Definition c_types.cpp:235

ait

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

auxiliary_symbolt

Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...

Definition symbol.h:153

code_typet::parameters

const parameterst & parameters() const

Definition std_types.h:698

dereference_exprt

Operator to dereference a pointer.

Definition pointer_expr.h:834

dstringt

dstringt has one field, an unsigned integer no which is an index into a static table of strings.

Definition dstring.h:38

dstringt::empty

bool empty() const

Definition dstring.h:101

exprt

Base class for all expressions.

Definition expr.h:57

exprt::operandst

std::vector< exprt > operandst

Definition expr.h:59

exprt::operands

operandst & operands()

Definition expr.h:95

exprt::add_source_location

source_locationt & add_source_location()

Definition expr.h:241

function_application_exprt

Application of (mathematical) function.

Definition mathematical_expr.h:213

irept::get

const irep_idt & get(const irep_idt &name) const

Definition irep.cpp:44

irept::set

void set(const irep_idt &name, const irep_idt &value)

Definition irep.h:412

irept::id

const irep_idt & id() const

Definition irep.h:388

java_class_typet

Definition java_types.h:196

java_method_typet

Definition java_types.h:100

java_string_library_preprocesst::implements_java_char_sequence

static bool implements_java_char_sequence(const typet &type)

Definition java_string_library_preprocess.h:75

mathematical_function_typet

A type for mathematical functions (do not confuse with functions/methods in code)

Definition mathematical_types.h:74

message_handlert

Definition message.h:27

messaget

Class that provides messages with a built-in verbosity 'level'.

Definition message.h:154

messaget::warning

mstreamt & warning() const

Definition message.h:406

messaget::eom

static eomt eom

Definition message.h:289

pointer_typet

The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...

Definition pointer_expr.h:24

resolve_inherited_componentt

Definition resolve_inherited_component.h:25

source_locationt

Definition source_location.h:20

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:76

struct_tag_typet

A struct tag type, i.e., struct_typet with an identifier.

Definition std_types.h:492

struct_typet

Structure type, corresponds to C style structs.

Definition std_types.h:230

struct_union_typet::componentst

std::vector< componentt > componentst

Definition std_types.h:139

symbol_table_baset

The symbol table base class interface.

Definition symbol_table_base.h:23

symbol_table_baset::insert

virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0

Move or copy a new symbol to the symbol table.

symbol_table_baset::symbols

const symbolst & symbols

Read-only field, used to look up symbols given their names.

Definition symbol_table_base.h:31

symbol_table_baset::add

bool add(const symbolt &symbol)

Add a new symbol to the symbol table.

Definition symbol_table_base.cpp:18

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:105

symbolt

Symbol table entry.

Definition symbol.h:28

symbolt::type

typet type

Type of symbol.

Definition symbol.h:31

type_symbolt

Symbol table entry describing a data typeThis is a symbol generated as part of type checking.

Definition symbol.h:139

typet

The type of an expression, extends irept.

Definition type.h:29

has_prefix

bool has_prefix(const std::string &s, const std::string &prefix)

Definition converter.cpp:13

err

void err(int eval, const char *fmt,...)

Definition err.c:13

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

fresh_symbol.h

Fresh auxiliary symbol creation.

id2string

const std::string & id2string(const irep_idt &d)

Definition irep.h:44

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:20

java_root_class.h

java_string_library_preprocess.h

Produce code for simple implementation of String Java libraries.

java_int_type

signedbv_typet java_int_type()

Definition java_types.cpp:31

java_byte_type

signedbv_typet java_byte_type()

Definition java_types.cpp:55

java_short_type

signedbv_typet java_short_type()

Definition java_types.cpp:49

java_double_type

floatbv_typet java_double_type()

Definition java_types.cpp:73

java_float_type

floatbv_typet java_float_type()

Definition java_types.cpp:67

java_boolean_type

c_bool_typet java_boolean_type()

Definition java_types.cpp:79

java_char_type

unsignedbv_typet java_char_type()

Definition java_types.cpp:61

java_long_type

signedbv_typet java_long_type()

Definition java_types.cpp:43

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 (for examp...

Definition java_utils.cpp:114

is_java_string_literal_id

bool is_java_string_literal_id(const irep_idt &id)

Definition java_utils.cpp:207

get_java_primitive_type_info

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:63

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:341

get_boxed_type_info_by_name

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:36

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:529

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:519

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:212

declaring_class

std::optional< irep_idt > declaring_class(const symbolt &symbol)

Gets the identifier of the class which declared a given symbol.

Definition java_utils.cpp:568

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:358

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:574

is_primitive_wrapper_type_id

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:109

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:162

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:27

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:147

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:555

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:302

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:407

checked_dereference

dereference_exprt checked_dereference(const exprt &expr)

Dereference an expression and flag it for a null-pointer check.

Definition java_utils.cpp:281

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:384

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:269

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:128

class_name_from_method_name

std::optional< 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:580

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:198

java_class_to_package

const std::string java_class_to_package(const std::string &canonical_classname)

Definition java_utils.cpp:157

get_inherited_component

std::optional< resolve_inherited_componentt::inherited_componentt > get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const symbol_table_baset &symbol_table, bool include_interfaces)

Finds an inherited component (method or field), taking component visibility into account.

Definition java_utils.cpp:448

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:421

java_utils.h

JAVA_STRING_LITERAL_PREFIX

#define JAVA_STRING_LITERAL_PREFIX

Definition java_utils.h:103

mathematical_expr.h

API to expression classes for 'mathematical' expressions.

mathematical_types.h

Mathematical types.

prefix.h

invariant.h

UNREACHABLE

#define UNREACHABLE

This should be used to mark dead code.

Definition invariant.h:525

PRECONDITION

#define PRECONDITION(CONDITION)

Definition invariant.h:463

INVARIANT

#define INVARIANT(CONDITION, REASON)

This macro uses the wrapper function 'invariant_violated_string'.

Definition invariant.h:423

message.h

std_types.h

Pre-defined types.

to_struct_type

const struct_typet & to_struct_type(const typet &type)

Cast a typet to a struct_typet.

Definition std_types.h:307

trim_from_last_delimiter

std::string trim_from_last_delimiter(std::string_view s, const char delim)

Definition string_utils.cpp:131

string_utils.h

java_boxed_type_infot

Return type for get_boxed_type_info_by_name.

Definition java_utils.h:53

java_primitive_type_infot

Return type for get_java_primitive_type_info.

Definition java_utils.h:33

symbol_table_base.h

Author: Diffblue Ltd.

irep_idt

dstringt irep_idt

Definition verification_result.h:16