cprover
refined_string_type.h
Go to the documentation of this file.
1 /********************************************************************\
2 
3 Module: 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 
9 Author: 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 "std_types.h"
24 
25 // Internal type used for string refinement
27 {
28 public:
30 
31  // Type for the content (list of characters) of a string
32  const typet &get_content_type() const
33  {
34  PRECONDITION(components().size()==2);
35  return components()[1].type();
36  }
37 
38  const typet &get_char_type() const
39  {
40  return get_content_type().subtype();
41  }
42 
43  const typet &get_index_type() const
44  {
45  PRECONDITION(components().size()==2);
46  return components()[0].type();
47  }
48 };
49 
50 inline bool is_refined_string_type(const typet &type)
51 {
52  return
53  type.id()==ID_struct &&
54  to_struct_type(type).get_tag()==CPROVER_PREFIX"refined_string_type";
55 }
56 
58  const typet &type)
59 {
61  return static_cast<const refined_string_typet &>(type);
62 }
63 
64 #endif
The type of an expression.
Definition: type.h:22
const typet & get_char_type() const
#define CPROVER_PREFIX
const componentst & components() const
Definition: std_types.h:245
Structure type.
Definition: std_types.h:297
const irep_idt & id() const
Definition: irep.h:189
const refined_string_typet & to_refined_string_type(const typet &type)
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
const typet & get_content_type() const
const typet & get_index_type() const
bitvector_typet index_type()
Definition: c_types.cpp:16
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
API to type classes.
bool is_refined_string_type(const typet &type)
const typet & subtype() const
Definition: type.h:33
irep_idt get_tag() const
Definition: std_types.h:266
refined_string_typet(const typet &index_type, const typet &char_type)
bitvector_typet char_type()
Definition: c_types.cpp:114