|
CBMC
|
#include "bv_utils.h"
Include dependency graph for bv_utils.cpp:Go to the source code of this file.
Macros | |
| #define | OPTIMAL_FULL_ADDER |
| Generates the encoding of a full adder. More... | |
| #define | COMPACT_CARRY |
| #define | COMPACT_LT_OR_LE |
| To provide a bitwise model of < or <=. More... | |
| #define COMPACT_CARRY |
Definition at line 225 of file bv_utils.cpp.
| #define COMPACT_LT_OR_LE |
To provide a bitwise model of < or <=.
Definition at line 1194 of file bv_utils.cpp.
| #define OPTIMAL_FULL_ADDER |
Generates the encoding of a full adder.
The optimal encoding is the default.
Definition at line 134 of file bv_utils.cpp.