CBMC
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 
22  const typet &index_type,
23  const pointer_typet &content_type)
24  : struct_typet({{"length", index_type}, {"content", content_type}})
25 {
26  set_tag(CPROVER_PREFIX"refined_string_type");
27 }
typet
The type of an expression, extends irept.
Definition: type.h:28
index_type
bitvector_typet index_type()
Definition: c_types.cpp:22
refined_string_typet::refined_string_typet
refined_string_typet(const typet &index_type, const pointer_typet &content_type)
Definition: refined_string_type.cpp:21
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:230
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: pointer_expr.h:23