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
jsil_reference_type
typet jsil_reference_type()
Definition: jsil_types.cpp:46
jsil_object_type
typet jsil_object_type()
Definition: jsil_types.cpp:62
jsil_prim_type
typet jsil_prim_type()
Definition: jsil_types.cpp:41
jsil_user_object_type
typet jsil_user_object_type()
Definition: jsil_types.cpp:68
jsil_kind
typet jsil_kind()
Definition: jsil_types.cpp:88
typet
The type of an expression, extends irept.
Definition: type.h:29
jsil_value_or_reference_type
typet jsil_value_or_reference_type()
Definition: jsil_types.cpp:27
jsil_union_typet::intersect_with
jsil_union_typet intersect_with(const jsil_union_typet &other) const
Definition: jsil_types.cpp:167
to_jsil_builtin_code_type
jsil_builtin_code_typet & to_jsil_builtin_code_type(code_typet &code)
Definition: jsil_types.h:48
jsil_union_typet
Definition: jsil_types.h:85
jsil_null_type
typet jsil_null_type()
Definition: jsil_types.cpp:78
jsil_builtin_code_typet::jsil_builtin_code_typet
jsil_builtin_code_typet(code_typet &code)
Definition: jsil_types.h:41
jsil_union_typet::to_type
const typet & to_type() const
Definition: jsil_types.cpp:217
jsil_empty_type
typet jsil_empty_type()
Definition: jsil_types.cpp:93
jsil_value_or_empty_type
typet jsil_value_or_empty_type()
Definition: jsil_types.cpp:22
type.h
Defines typet, type_with_subtypet and type_with_subtypest.
jsil_is_subtype
bool jsil_is_subtype(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:98
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
to_jsil_spec_code_type
jsil_spec_code_typet & to_jsil_spec_code_type(code_typet &code)
Definition: jsil_types.h:71
jsil_builtin_object_type
typet jsil_builtin_object_type()
Definition: jsil_types.cpp:73
jsil_value_type
typet jsil_value_type()
Definition: jsil_types.cpp:32
std_types.h
Pre-defined types.
jsil_union
typet jsil_union(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:119
code_typet
Base type of functions.
Definition: std_types.h:736
irept::id
const irep_idt & id() const
Definition: irep.h:418
union_typet
The union type.
Definition: std_types.h:393
jsil_union_typet::is_subtype
bool is_subtype(const jsil_union_typet &other) const
Definition: jsil_types.cpp:184
jsil_union_typet::jsil_union_typet
jsil_union_typet(const typet &type)
Definition: jsil_types.h:89
jsil_union_typet::jsil_union_typet
jsil_union_typet()
Definition: jsil_types.h:87
jsil_variable_reference_type
typet jsil_variable_reference_type()
Definition: jsil_types.cpp:57
to_jsil_union_type
jsil_union_typet & to_jsil_union_type(typet &type)
Definition: jsil_types.h:103
jsil_builtin_code_typet
Definition: jsil_types.h:39
is_jsil_builtin_code_type
bool is_jsil_builtin_code_type(const typet &type)
Definition: jsil_types.h:55
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
jsil_spec_code_typet
Definition: jsil_types.h:62
jsil_union_typet::union_with
jsil_union_typet union_with(const jsil_union_typet &other) const
Definition: jsil_types.cpp:150
jsil_spec_code_typet::jsil_spec_code_typet
jsil_spec_code_typet(code_typet &code)
Definition: jsil_types.h:64
is_jsil_spec_code_type
bool is_jsil_spec_code_type(const typet &type)
Definition: jsil_types.h:78
jsil_incompatible_types
bool jsil_incompatible_types(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:113
jsil_undefined_type
typet jsil_undefined_type()
Definition: jsil_types.cpp:83
jsil_member_reference_type
typet jsil_member_reference_type()
Definition: jsil_types.cpp:52
jsil_any_type
typet jsil_any_type()
Definition: jsil_types.cpp:16