CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
java_bytecode_parser.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
19struct java_bytecode_parse_treet;
20
28std::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
41std::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
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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