cprover
Loading...
Searching...
No Matches
jsil_types.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Jsil Language
4
5Author: 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/c_types.h>
16
32
33bool jsil_is_subtype(const typet &type1, const typet &type2);
34bool jsil_incompatible_types(const typet &type1, const typet &type2);
35typet jsil_union(const typet &type1, const typet &type2);
36
38{
39public:
41 code_typet(code)
42 {
43 set("jsil_builtin_proceduret", true);
44 }
45};
46
48 code_typet &code)
49{
50 PRECONDITION(code.get_bool("jsil_builtin_proceduret"));
51 return static_cast<jsil_builtin_code_typet &>(code);
52}
53
54inline bool is_jsil_builtin_code_type(const typet &type)
55{
56 return type.id()==ID_code &&
57 type.get_bool("jsil_builtin_proceduret");
58}
59
61{
62public:
64 code_typet(code)
65 {
66 set("jsil_spec_proceduret", true);
67 }
68};
69
71 code_typet &code)
72{
73 PRECONDITION(code.get_bool("jsil_spec_proceduret"));
74 return static_cast<jsil_spec_code_typet &>(code);
75}
76
77inline bool is_jsil_spec_code_type(const typet &type)
78{
79 return type.id()==ID_code &&
80 type.get_bool("jsil_spec_proceduret");
81}
82
84{
85public:
87
88 explicit jsil_union_typet(const typet &type)
89 :jsil_union_typet(std::vector<typet>({type})) { }
90
91 explicit jsil_union_typet(const std::vector<typet> &types);
92
94
96
97 bool is_subtype(const jsil_union_typet &other) const;
98
99 const typet &to_type() const;
100};
101
103{
104 PRECONDITION(type.id() == ID_union);
105 return static_cast<jsil_union_typet &>(type);
106}
107
108inline const jsil_union_typet &to_jsil_union_type(const typet &type)
109{
110 PRECONDITION(type.id() == ID_union);
111 return static_cast<const jsil_union_typet &>(type);
112}
113
114#endif // CPROVER_JSIL_JSIL_TYPES_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Base type of functions.
Definition std_types.h:539
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
const irep_idt & id() const
Definition irep.h:396
jsil_builtin_code_typet(code_typet &code)
Definition jsil_types.h:40
jsil_spec_code_typet(code_typet &code)
Definition jsil_types.h:63
jsil_union_typet union_with(const jsil_union_typet &other) const
jsil_union_typet(const typet &type)
Definition jsil_types.h:88
jsil_union_typet intersect_with(const jsil_union_typet &other) const
bool is_subtype(const jsil_union_typet &other) const
const typet & to_type() const
The type of an expression, extends irept.
Definition type.h:29
The union type.
Definition c_types.h:147
typet jsil_value_or_empty_type()
typet jsil_empty_type()
typet jsil_undefined_type()
typet jsil_null_type()
typet jsil_variable_reference_type()
bool jsil_is_subtype(const typet &type1, const typet &type2)
bool is_jsil_spec_code_type(const typet &type)
Definition jsil_types.h:77
typet jsil_kind()
typet jsil_builtin_object_type()
typet jsil_user_object_type()
typet jsil_union(const typet &type1, const typet &type2)
bool jsil_incompatible_types(const typet &type1, const typet &type2)
jsil_union_typet & to_jsil_union_type(typet &type)
Definition jsil_types.h:102
jsil_builtin_code_typet & to_jsil_builtin_code_type(code_typet &code)
Definition jsil_types.h:47
typet jsil_prim_type()
bool is_jsil_builtin_code_type(const typet &type)
Definition jsil_types.h:54
typet jsil_any_type()
typet jsil_reference_type()
typet jsil_member_reference_type()
typet jsil_value_or_reference_type()
jsil_spec_code_typet & to_jsil_spec_code_type(code_typet &code)
Definition jsil_types.h:70
typet jsil_value_type()
typet jsil_object_type()
STL namespace.
#define PRECONDITION(CONDITION)
Definition invariant.h:463