cprover
jsil_types.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Jsil Language
4 
5 Author: Daiva Naudziuniene, daivan@amazon.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_JSIL_JSIL_TYPES_H
13 #define CPROVER_JSIL_JSIL_TYPES_H
14 
15 #include <util/type.h>
16 #include <util/std_types.h>
17 
33 
34 bool jsil_is_subtype(const typet &type1, const typet &type2);
35 bool jsil_incompatible_types(const typet &type1, const typet &type2);
36 typet jsil_union(const typet &type1, const typet &type2);
37 
39 {
40 public:
42  code_typet(code)
43  {
44  set("jsil_builtin_proceduret", true);
45  }
46 };
47 
49  code_typet &code)
50 {
51  assert(code.get_bool("jsil_builtin_proceduret"));
52  return static_cast<jsil_builtin_code_typet &>(code);
53 }
54 
55 inline bool is_jsil_builtin_code_type(const typet &type)
56 {
57  return type.id()==ID_code &&
58  type.get_bool("jsil_builtin_proceduret");
59 }
60 
62 {
63 public:
65  code_typet(code)
66  {
67  set("jsil_spec_proceduret", true);
68  }
69 };
70 
72  code_typet &code)
73 {
74  assert(code.get_bool("jsil_spec_proceduret"));
75  return static_cast<jsil_spec_code_typet &>(code);
76 }
77 
78 inline bool is_jsil_spec_code_type(const typet &type)
79 {
80  return type.id()==ID_code &&
81  type.get_bool("jsil_spec_proceduret");
82 }
83 
85 {
86 public:
88 
89  explicit jsil_union_typet(const typet &type)
90  :jsil_union_typet(std::vector<typet>({type})) { }
91 
92  explicit jsil_union_typet(const std::vector<typet> &types);
93 
94  jsil_union_typet union_with(const jsil_union_typet &other) const;
95 
97 
98  bool is_subtype(const jsil_union_typet &other) const;
99 
100  const typet &to_type() const;
101 };
102 
104 {
105  assert(type.id()==ID_union);
106  return static_cast<jsil_union_typet &>(type);
107 }
108 
109 inline const jsil_union_typet &to_jsil_union_type(const typet &type)
110 {
111  assert(type.id()==ID_union);
112  return static_cast<const jsil_union_typet &>(type);
113 }
114 
115 #endif // CPROVER_JSIL_JSIL_TYPES_H
The type of an expression, extends irept.
Definition: type.h:27
Base type of functions.
Definition: std_types.h:751
bool jsil_incompatible_types(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:113
typet jsil_object_type()
Definition: jsil_types.cpp:62
typet jsil_empty_type()
Definition: jsil_types.cpp:93
typet jsil_reference_type()
Definition: jsil_types.cpp:46
jsil_union_typet intersect_with(const jsil_union_typet &other) const
Definition: jsil_types.cpp:167
jsil_union_typet union_with(const jsil_union_typet &other) const
Definition: jsil_types.cpp:150
typet jsil_variable_reference_type()
Definition: jsil_types.cpp:57
STL namespace.
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
bool is_jsil_spec_code_type(const typet &type)
Definition: jsil_types.h:78
jsil_builtin_code_typet(code_typet &code)
Definition: jsil_types.h:41
const irep_idt & id() const
Definition: irep.h:259
typet jsil_builtin_object_type()
Definition: jsil_types.cpp:73
typet jsil_value_or_empty_type()
Definition: jsil_types.cpp:22
typet jsil_member_reference_type()
Definition: jsil_types.cpp:52
typet jsil_union(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:119
const typet & to_type() const
Definition: jsil_types.cpp:217
typet jsil_user_object_type()
Definition: jsil_types.cpp:68
jsil_union_typet(const typet &type)
Definition: jsil_types.h:89
typet jsil_prim_type()
Definition: jsil_types.cpp:41
bool is_jsil_builtin_code_type(const typet &type)
Definition: jsil_types.h:55
jsil_spec_code_typet & to_jsil_spec_code_type(code_typet &code)
Definition: jsil_types.h:71
jsil_builtin_code_typet & to_jsil_builtin_code_type(code_typet &code)
Definition: jsil_types.h:48
Pre-defined types.
typet jsil_null_type()
Definition: jsil_types.cpp:78
typet jsil_value_or_reference_type()
Definition: jsil_types.cpp:27
typet jsil_any_type()
Definition: jsil_types.cpp:16
The union type.
Definition: std_types.h:425
typet jsil_kind()
Definition: jsil_types.cpp:88
typet jsil_undefined_type()
Definition: jsil_types.cpp:83
typet jsil_value_type()
Definition: jsil_types.cpp:32
bool is_subtype(const jsil_union_typet &other) const
Definition: jsil_types.cpp:184
bool jsil_is_subtype(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:98
jsil_spec_code_typet(code_typet &code)
Definition: jsil_types.h:64
jsil_union_typet & to_jsil_union_type(typet &type)
Definition: jsil_types.h:103
Defines typet, type_with_subtypet and type_with_subtypest.