CBMC
java_bytecode_parser.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSER_H
11 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSER_H
12 
13 #include <util/irep.h>
14 
15 #include <iosfwd>
16 #include <optional>
17 #include <string>
18 
19 struct java_bytecode_parse_treet;
20 
28 std::optional<java_bytecode_parse_treet> java_bytecode_parse(
29  const std::string &file,
30  const irep_idt &class_name,
31  class message_handlert &msg,
32  bool skip_instructions = false);
33 
41 std::optional<java_bytecode_parse_treet> java_bytecode_parse(
42  std::istream &stream,
43  const irep_idt &class_name,
44  class message_handlert &msg,
45  bool skip_instructions = false);
46 
47 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSER_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
message_handlert
Definition: message.h:27
java_bytecode_parse
std::optional< java_bytecode_parse_treet > java_bytecode_parse(const std::string &file, const irep_idt &class_name, class message_handlert &msg, bool skip_instructions=false)
Attempt to parse a Java class from the given file.
Definition: java_bytecode_parser.cpp:1830
java_bytecode_parse_treet
Definition: java_bytecode_parse_tree.h:23