File tree Expand file tree Collapse file tree 3 files changed +28
-17
lines changed
Expand file tree Collapse file tree 3 files changed +28
-17
lines changed Original file line number Diff line number Diff line change @@ -14,7 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com
1414#include < cassert>
1515#include < iosfwd>
1616
17- #define USE_DSTRING
17+ #include " irep_ids.h"
18+
1819#define SHARING
1920// #define HASH_CODE
2021#define USE_MOVE
@@ -26,12 +27,6 @@ Author: Daniel Kroening, kroening@kroening.com
2627#include < map>
2728#endif
2829
29- #ifdef USE_DSTRING
30- #include " dstring.h"
31- #endif
32-
33- #include " irep_ids.h"
34-
3530#ifdef USE_DSTRING
3631typedef dstringt irep_idt;
3732typedef dstringt irep_namet;
Original file line number Diff line number Diff line change @@ -21,6 +21,24 @@ const char *irep_ids_table[]=
2121 NULL ,
2222};
2323
24+ #ifdef USE_DSTRING
25+
26+ #define IREP_ID_ONE (the_id ) \
27+ const dstringt ID_##the_id=dstringt::make_from_table_index( \
28+ static_cast <unsigned >(idt::id_##the_id));
29+ #define IREP_ID_TWO (the_id, str ) \
30+ const dstringt ID_##the_id=dstringt::make_from_table_index( \
31+ static_cast <unsigned >(idt::id_##the_id));
32+
33+ #else
34+
35+ #define IREP_ID_ONE (the_id ) const std::string ID_##the_id(#the_id);
36+ #define IREP_ID_TWO (the_id, str ) const std::string ID_##the_id(#the_id);
37+
38+ #endif
39+
40+ #include " irep_ids.def" // NOLINT(build/include)
41+
2442/* ******************************************************************\
2543
2644Function: initialize_string_container
Original file line number Diff line number Diff line change @@ -9,7 +9,11 @@ Author: Reuben Thomas, reuben.thomas@me.com
99#ifndef CPROVER_UTIL_IREP_IDS_H
1010#define CPROVER_UTIL_IREP_IDS_H
1111
12+ #define USE_DSTRING
13+
14+ #ifdef USE_DSTRING
1215#include " dstring.h"
16+ #endif
1317
1418enum class idt :unsigned
1519{
@@ -21,19 +25,13 @@ enum class idt:unsigned
2125
2226#ifdef USE_DSTRING
2327
24- #define IREP_ID_ONE (the_id ) \
25- static const dstringt ID_##the_id= \
26- dstringt::make_from_table_index (static_cast <unsigned >(idt::id_##the_id));
27- #define IREP_ID_TWO (the_id, str ) \
28- static const dstringt ID_##the_id= \
29- dstringt::make_from_table_index (static_cast <unsigned >(idt::id_##the_id));
28+ #define IREP_ID_ONE (the_id ) extern const dstringt ID_##the_id;
29+ #define IREP_ID_TWO (the_id, str ) extern const dstringt ID_##the_id;
3030
3131#else
3232
33- #define IREP_ID_ONE (the_id ) \
34- static const std::string ID_##the_id(#the_id);
35- #define IREP_ID_TWO (the_id, str ) \
36- static const std::string ID_##the_id(#the_id);
33+ #define IREP_ID_ONE (the_id ) extern const std::string ID_##the_id;
34+ #define IREP_ID_TWO (the_id, str ) extern const std::string ID_##the_id;
3735
3836#endif
3937
You can’t perform that action at this time.
0 commit comments