CBMC
util.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop Acceleration
4 
5 Author: Matt Lewis
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_UTIL_H
13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_UTIL_H
14 
15 #include <util/bitvector_types.h>
16 
17 signedbv_typet signed_poly_type();
18 unsignedbv_typet unsigned_poly_type();
19 
20 bool is_bitvector(const typet &t);
21 typet join_types(const typet &t1, const typet &t2);
22 
23 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_UTIL_H
bitvector_types.h
Pre-defined bitvector types.
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: bitvector_types.h:212
typet
The type of an expression, extends irept.
Definition: type.h:29
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: bitvector_types.h:163
join_types
typet join_types(const typet &t1, const typet &t2)
Return the smallest type that both t1 and t2 can be cast to without losing information.
Definition: util.cpp:70
unsigned_poly_type
unsignedbv_typet unsigned_poly_type()
Definition: util.cpp:25
is_bitvector
bool is_bitvector(const typet &t)
Convenience function – is the type a bitvector of some kind?
Definition: util.cpp:33
signed_poly_type
signedbv_typet signed_poly_type()
Definition: util.cpp:20