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
23
refined_string_typet::refined_string_typet
(
24
const
typet
&
index_type
,
25
const
pointer_typet
&content_type)
26
{
27
components
().emplace_back(
"length"
,
index_type
);
28
components
().emplace_back(
"content"
, content_type);
29
set_tag
(
CPROVER_PREFIX
"refined_string_type"
);
30
}
struct_union_typet::components
const componentst & components() const
Definition:
std_types.h:205
typet
The type of an expression, extends irept.
Definition:
type.h:27
index_type
bitvector_typet index_type()
Definition:
c_types.cpp:16
struct_union_typet::set_tag
void set_tag(const irep_idt &tag)
Definition:
std_types.h:227
refined_string_typet::refined_string_typet
refined_string_typet(const typet &index_type, const pointer_typet &content_type)
Definition:
refined_string_type.cpp:23
refined_string_type.h
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition:
cprover_prefix.h:14
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition:
std_types.h:1507
std_expr.h
util
refined_string_type.cpp
Generated by
1.8.16