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 
96  jsil_union_typet intersect_with(const jsil_union_typet &other) const;
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.
Definition: type.h:20
Base type of functions.
Definition: std_types.h:734
bool jsil_incompatible_types(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:131
typet jsil_object_type()
Definition: jsil_types.cpp:78
typet jsil_empty_type()
Definition: jsil_types.cpp:111
typet jsil_reference_type()
Definition: jsil_types.cpp:60
typet jsil_variable_reference_type()
Definition: jsil_types.cpp:73
STL namespace.
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
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:189
typet jsil_builtin_object_type()
Definition: jsil_types.cpp:91
typet jsil_value_or_empty_type()
Definition: jsil_types.cpp:25
typet jsil_member_reference_type()
Definition: jsil_types.cpp:68
typet jsil_union(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:137
typet jsil_user_object_type()
Definition: jsil_types.cpp:86
jsil_union_typet(const typet &type)
Definition: jsil_types.h:89
typet jsil_prim_type()
Definition: jsil_types.cpp:51
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
API to type classes.
typet jsil_null_type()
Definition: jsil_types.cpp:96
typet jsil_value_or_reference_type()
Definition: jsil_types.cpp:33
typet jsil_any_type()
Definition: jsil_types.cpp:16
The union type.
Definition: std_types.h:424
typet jsil_kind()
Definition: jsil_types.cpp:106
typet jsil_undefined_type()
Definition: jsil_types.cpp:101
typet jsil_value_type()
Definition: jsil_types.cpp:41
bool jsil_is_subtype(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:116
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