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
typet
The type of an expression, extends irept.
Definition:
type.h:28
unsigned_poly_type
unsignedbv_typet unsigned_poly_type()
Definition:
util.cpp:25
signed_poly_type
signedbv_typet signed_poly_type()
Definition:
util.cpp:20
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition:
bitvector_types.h:158
bitvector_types.h
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition:
bitvector_types.h:207
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
is_bitvector
bool is_bitvector(const typet &t)
Convenience function – is the type a bitvector of some kind?
Definition:
util.cpp:33
src
goto-instrument
accelerate
util.h
Generated by
1.8.17