cprover
byte_operators.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "byte_operators.h"
10 
11 #include "config.h"
12 
14 {
15  switch(config.ansi_c.endianness)
16  {
18  return ID_byte_extract_little_endian;
19 
21  return ID_byte_extract_big_endian;
22 
25  }
26 
28 }
29 
31 {
32  switch(config.ansi_c.endianness)
33  {
35  return ID_byte_update_little_endian;
36 
38  return ID_byte_update_big_endian;
39 
42  }
43 
45 }
46 
48 make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
49 {
50  return byte_extract_exprt{byte_extract_id(), _op, _offset, _type};
51 }
52 
54 make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value)
55 {
56  return byte_update_exprt{byte_update_id(), _op, _offset, _value};
57 }
Expression classes for byte-level operators.
Expression of type type extracted from some object op starting at position offset (given in number of...
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
The type of an expression, extends irept.
Definition: type.h:28
configt config
Definition: config.cpp:25
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
endiannesst endianness
Definition: config.h:156
static irep_idt byte_extract_id()
byte_update_exprt make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value)
Construct a byte_update_exprt with endianness and byte width matching the current configuration.
static irep_idt byte_update_id()
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.