cprover
java_bytecode_language.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_LANGUAGE_H
11 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H
12 
13 #include <util/language.h>
14 #include <util/cmdline.h>
15 
16 #include "java_class_loader.h"
18 
19 #define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5
20 
21 class symbolt;
22 
24 {
28 };
29 
30 typedef std::pair<
31  const symbolt *,
34 typedef std::map<irep_idt, lazy_method_valuet>
36 
38 {
39 public:
40  virtual void get_language_options(const cmdlinet &) override;
41 
42  virtual bool preprocess(
43  std::istream &instream,
44  const std::string &path,
45  std::ostream &outstream) override;
46 
47  bool parse(
48  std::istream &instream,
49  const std::string &path) override;
50 
51  bool typecheck(
52  symbol_tablet &context,
53  const std::string &module) override;
54 
55  bool final(
56  symbol_tablet &context) override;
57 
58  void show_parse(std::ostream &out) override;
59 
60  virtual ~java_bytecode_languaget();
64  {}
65 
66  bool from_expr(
67  const exprt &expr,
68  std::string &code,
69  const namespacet &ns) override;
70 
71  bool from_type(
72  const typet &type,
73  std::string &code,
74  const namespacet &ns) override;
75 
76  bool to_expr(
77  const std::string &code,
78  const std::string &module,
79  exprt &expr,
80  const namespacet &ns) override;
81 
82  languaget *new_language() override
83  { return new java_bytecode_languaget; }
84 
85  std::string id() const override { return "java"; }
86  std::string description() const override { return "Java Bytecode"; }
87  std::set<std::string> extensions() const override;
88 
89  void modules_provided(std::set<std::string> &modules) override;
90  virtual void lazy_methods_provided(std::set<irep_idt> &) const override;
91  virtual void convert_lazy_method(
92  const irep_idt &id, symbol_tablet &) override;
93 
94 protected:
96 
98  std::vector<irep_idt> main_jar_classes;
100  bool assume_inputs_non_null; // assume inputs variables to be non-null
101  size_t max_nondet_array_length; // maximal length for non-det array creation
102  size_t max_user_array_length; // max size for user code created arrays
108 };
109 
111 
112 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H
The type of an expression.
Definition: type.h:20
java_class_loadert java_class_loader
void modules_provided(std::set< std::string > &modules) override
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
void show_parse(std::ostream &out) override
Preprocess a goto-programs so that calls to the java Character library are replaced by simple express...
virtual void lazy_methods_provided(std::set< irep_idt > &) const override
Provide feedback to language_filest so that when asked for a lazy method, it can delegate to this ins...
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
std::set< std::string > extensions() const override
lazy_methods_modet
languaget * new_language() override
character_refine_preprocesst character_preprocess
virtual void get_language_options(const cmdlinet &) override
Consume options that are java bytecode specific.
bool typecheck(symbol_tablet &context, const std::string &module) override
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Abstract interface to support a programming language.
std::string id() const override
std::string description() const override
std::map< irep_idt, lazy_method_valuet > lazy_methodst
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
virtual void convert_lazy_method(const irep_idt &id, symbol_tablet &) override
Promote a lazy-converted method (one whose type is known but whose body hasn&#39;t been converted) into a...
#define MAX_NONDET_ARRAY_LENGTH_DEFAULT
Base class for all expressions.
Definition: expr.h:46
bool parse(std::istream &instream, const std::string &path) override
languaget * new_java_bytecode_language()
lazy_methods_modet lazy_methods_mode
std::pair< const symbolt *, const java_bytecode_parse_treet::methodt * > lazy_method_valuet
bool do_ci_lazy_method_conversion(symbol_tablet &, lazy_methodst &)
Uses a simple context-insensitive (&#39;ci&#39;) analysis to determine which methods may be reachable from th...
std::vector< irep_idt > main_jar_classes