CBMC: /home/runner/work/cbmc/cbmc/src/goto-instrument/accelerate/util.h Source File

CBMC
Loading...
Searching...
No Matches
util.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Loop Acceleration
4
5Author: 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
17signedbv_typet signed_poly_type();
18unsignedbv_typet unsigned_poly_type();
19
20bool is_bitvector(const typet &t);
21typet join_types(const typet &t1, const typet &t2);
22
23#endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_UTIL_H
Pre-defined bitvector types.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
Fixed-width bit-vector with two's complement interpretation.
The type of an expression, extends irept.
Definition type.h:29
Fixed-width bit-vector with unsigned binary interpretation.
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
unsignedbv_typet unsigned_poly_type()
Definition util.cpp:25
bool is_bitvector(const typet &t)
Convenience function – is the type a bitvector of some kind?
Definition util.cpp:33
signedbv_typet signed_poly_type()
Definition util.cpp:20

AltStyle によって変換されたページ (->オリジナル) /