CBMC
|
#include "enum_encoding.h"
#include <util/c_types.h>
#include <util/expr_cast.h>
#include <util/namespace.h>
#include <queue>
Go to the source code of this file.
Functions | |
static typet | encode (typet type, const namespacet &ns) |
exprt | lower_enum (exprt expr, const namespacet &ns) |
Function to lower expr and its sub-expressions containing enum types. More... | |
|
static |
Definition at line 13 of file enum_encoding.cpp.
exprt lower_enum | ( | exprt | expr, |
const namespacet & | ns | ||
) |
Function to lower expr
and its sub-expressions containing enum types.
Specifically it replaces the node c_enum_tag_typet
type with the underlying type of the enum the tag points to.
expr | the expression to lower. |
ns | the namespace where to lookup c_enum_tag_type s. |
Definition at line 37 of file enum_encoding.cpp.