CBMC
Loading...
Searching...
No Matches
Functions
util.h File Reference

Loop Acceleration. More...

#include <util/bitvector_types.h>
+ Include dependency graph for util.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

signedbv_typet  signed_poly_type ()
 
unsignedbv_typet  unsigned_poly_type ()
 
bool  is_bitvector (const typet &t)
  Convenience function – is the type a bitvector of some kind?
 
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.
 

Detailed Description

Loop Acceleration.

Definition in file util.h.

Function Documentation

◆  is_bitvector()

bool is_bitvector ( const typet &  t )

Convenience function – is the type a bitvector of some kind?

Definition at line 33 of file util.cpp.

◆  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.

e.g.

join_types(unsignedbv_typet(32), unsignedbv_typet(16))=unsignedbv_typet(32) join_types(signedbv_typet(16), unsignedbv_typet(16))=signedbv_typet(17) join_types(signedbv_typet(32), signedbv_typet(32))=signedbv_typet(32)

Definition at line 70 of file util.cpp.

◆  signed_poly_type()

signedbv_typet signed_poly_type ( )

Definition at line 20 of file util.cpp.

◆  unsigned_poly_type()

unsignedbv_typet unsigned_poly_type ( )

Definition at line 25 of file util.cpp.

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