CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
irep_ids.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Internal Representation
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "irep_ids.h"
13
14#include "invariant.h"
15
16#include "string_container.h"
17
18const char *irep_ids_table[]=
19{
20#define IREP_ID_ONE(id) #id,
21#define IREP_ID_TWO(id, str) #str,
22
23#include "irep_ids.def"
24
25 nullptr,
26};
27
28enum class idt:unsigned
29{
30#define IREP_ID_ONE(the_id) id_##the_id,
31#define IREP_ID_TWO(the_id, str) id_##the_id,
32
33#include "irep_ids.def" // NOLINT(build/include)
34};
35
36#define IREP_ID_ONE(the_id) \
37 const dstringt ID_##the_id=dstringt::make_from_table_index( \
38 static_cast<unsigned>(idt::id_##the_id));
39#define IREP_ID_TWO(the_id, str) \
40 const dstringt ID_##the_id=dstringt::make_from_table_index( \
41 static_cast<unsigned>(idt::id_##the_id));
42
43#include "irep_ids.def" // NOLINT(build/include)
44
46{
47 // pre-allocate empty string -- this gets index 0
48 get("");
49
50 // allocate strings
51 for(unsigned i=0; irep_ids_table[i]!=nullptr; i++)
52 {
53 unsigned x=operator[](irep_ids_table[i]);
54 INVARIANT(x==i, "i-th element is inserted at position i"); // sanity check
55 }
56}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
unsigned get(const char *s)
unsigned operator[](const char *s)
const char * irep_ids_table[]
Definition irep_ids.cpp:18
idt
Definition irep_ids.cpp:29
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
Container for C-Strings.