cprover
Loading...
Searching...
No Matches
refined_string_type.h
Go to the documentation of this file.
1/********************************************************************\
2
3Module: Type for string expressions used by the string solver.
4 These string expressions contain a field `length`, of type
5 `index_type`, a field `content` of type `content_type`.
6 This module also defines functions to recognise the C and java
7 string types.
8
9Author: Romain Brenguier, romain.brenguier@diffblue.com
10
11\*******************************************************************/
12
18
19#ifndef CPROVER_UTIL_REFINED_STRING_TYPE_H
20#define CPROVER_UTIL_REFINED_STRING_TYPE_H
21
22#include "cprover_prefix.h"
23#include "pointer_expr.h"
24
25// Internal type used for string refinement
27{
28public:
30 const typet &index_type,
32
33 // Type for the content (list of characters) of a string
35 {
36 PRECONDITION(components().size()==2);
37 return to_array_type(components()[1].type());
38 }
39
40 const typet &get_char_type() const
41 {
43 }
44
45 const typet &get_index_type() const
46 {
47 PRECONDITION(components().size()==2);
48 return components()[0].type();
49 }
50};
51
52inline bool is_refined_string_type(const typet &type)
53{
54 return
55 type.id()==ID_struct &&
56 to_struct_type(type).get_tag()==CPROVER_PREFIX"refined_string_type";
57}
58
60 const typet &type)
61{
63 return static_cast<const refined_string_typet &>(type);
64}
65
66#endif
bitvector_typet index_type()
Definition c_types.cpp:22
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Arrays with given size.
Definition std_types.h:763
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:777
const irep_idt & id() const
Definition irep.h:396
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & get_index_type() const
const array_typet & get_content_type() const
const typet & get_char_type() const
Structure type, corresponds to C style structs.
Definition std_types.h:231
irep_idt get_tag() const
Definition std_types.h:168
const componentst & components() const
Definition std_types.h:147
The type of an expression, extends irept.
Definition type.h:29
#define CPROVER_PREFIX
API to expression classes for Pointers.
bool is_refined_string_type(const typet &type)
const refined_string_typet & to_refined_string_type(const typet &type)
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:832