cprover
refined_string_type.cpp
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 #include "refined_string_type.h"
20 
21 #include "std_expr.h"
22 
24  const typet &index_type, const typet &char_type)
25 {
27  components().emplace_back("length", index_type);
28  components().emplace_back("content", char_array);
29  set_tag(CPROVER_PREFIX"refined_string_type");
30 }
The type of an expression.
Definition: type.h:22
#define CPROVER_PREFIX
Type for string expressions used by the string solver.
const componentst & components() const
Definition: std_types.h:245
An expression denoting infinity.
Definition: std_expr.h:4694
API to expression classes.
void set_tag(const irep_idt &tag)
Definition: std_types.h:267
bitvector_typet index_type()
Definition: c_types.cpp:16
arrays with given size
Definition: std_types.h:1004
refined_string_typet(const typet &index_type, const typet &char_type)
bitvector_typet char_type()
Definition: c_types.cpp:114