cprover
expr2java.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_JAVA_BYTECODE_EXPR2JAVA_H
11 #define CPROVER_JAVA_BYTECODE_EXPR2JAVA_H
12 
13 #include <string>
14 #include <ansi-c/expr2c_class.h>
15 
16 class expr2javat:public expr2ct
17 {
18 public:
19  explicit expr2javat(const namespacet &_ns):expr2ct(_ns) { }
20 protected:
21  virtual std::string convert_with_precedence(
22  const exprt &src, unsigned &precedence);
23  virtual std::string convert_java_this(const exprt &src, unsigned precedence);
24  virtual std::string convert_java_instanceof(
25  const exprt &src,
26  unsigned precedence);
27  virtual std::string convert_java_new(const exprt &src, unsigned precedence);
28  virtual std::string convert_code_java_delete(
29  const exprt &src,
30  unsigned precedence);
31  virtual std::string convert_struct(const exprt &src, unsigned &precedence);
32  virtual std::string convert_code(const codet &src, unsigned indent);
33  virtual std::string convert_constant(
34  const constant_exprt &src,
35  unsigned &precedence);
36  virtual std::string convert_code_function_call(
37  const code_function_callt &src,
38  unsigned indent);
39 
40  virtual std::string convert_rec(
41  const typet &src,
42  const c_qualifierst &qualifiers,
43  const std::string &declarator);
44 
45  // length of string representation of Java Char
46  // representation is '\u0000'
47  const std::size_t char_representation_length=8;
48 };
49 
50 std::string expr2java(const exprt &expr, const namespacet &ns);
51 std::string type2java(const typet &type, const namespacet &ns);
52 
53 #endif // CPROVER_JAVA_BYTECODE_EXPR2JAVA_H
The type of an expression.
Definition: type.h:20
expr2javat(const namespacet &_ns)
Definition: expr2java.h:19
virtual std::string convert_java_new(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:336
virtual std::string convert_code_java_delete(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:361
virtual std::string convert_java_instanceof(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:323
A constant literal expression.
Definition: std_expr.h:3685
virtual std::string convert_struct(const exprt &src, unsigned &precedence)
Definition: expr2java.cpp:95
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
Definition: expr2java.cpp:159
std::string type2java(const typet &type, const namespacet &ns)
Definition: expr2java.cpp:438
TO_BE_DOCUMENTED.
Definition: namespace.h:62
A function call.
Definition: std_code.h:657
const namespacet & ns
Definition: expr2c_class.h:35
const std::size_t char_representation_length
Definition: expr2java.h:47
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
Definition: expr2java.cpp:380
Base class for all expressions.
Definition: expr.h:46
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:431
virtual std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
Definition: expr2java.cpp:25
virtual std::string convert_code(const codet &src, unsigned indent)
Definition: expr2java.cpp:415
A statement in a programming language.
Definition: std_code.h:19
virtual std::string convert_rec(const typet &src, const c_qualifierst &qualifiers, const std::string &declarator)
Definition: expr2java.cpp:242
virtual std::string convert_java_this(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:316