Make USE_DSTRING conditional and disable it in Ubuntu/Clang/DEBUG Travis job

This introduces a macro USE_STD_STRING that can be set to disable USE_DSTRING,
and thus the use of dstringt as the implementation of irep_idt. The
Ubuntu/Clang/DEBUG Travis stage sets this macro to avoid future changes breaking
the build when disabling USE_DSTRING.

Author: tautschnig

.travis.yml

@@ -142,7 +142,7 @@ jobs:
         - CCACHE_CPP2=yes
         - EXTRA_CXXFLAGS="-DNDEBUG"
 
-    # Ubuntu Linux with glibc using clang++-3.7, debug mode
+    # Ubuntu Linux with glibc using clang++-3.7, debug mode, disable USE_DSTRING
     - stage: Test different OS/CXX/Flags
       os: linux
       sudo: false
@@ -165,7 +165,7 @@ jobs:
       env:
         - COMPILER="ccache clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
         - CCACHE_CPP2=yes
-        - EXTRA_CXXFLAGS="-DDEBUG"
+        - EXTRA_CXXFLAGS="-DDEBUG -DUSE_STD_STRING"
       script: echo "Not running any tests for a debug build."
 
     # cmake build using g++-5

doc/architectural/cbmc-guide.md

@@ -597,5 +597,5 @@ they are in the code.
 [^2]: Or references, if reference counted data sharing is enabled. It is
     enabled by default; see the `SHARING` macro.
 
-[^3]: When `USE_DSTRING` is enabled (it is by default), this is actually
+[^3]: Unless `USE_STD_STRING` is set, this is actually
 a `dstring` and thus an integer which is a reference into a string table

src/util/irep_ids.h

@@ -12,7 +12,9 @@ Author: Reuben Thomas, [email protected]
 #ifndef CPROVER_UTIL_IREP_IDS_H
 #define CPROVER_UTIL_IREP_IDS_H
 
+#ifndef USE_STD_STRING
 #define USE_DSTRING
+#endif
 
 #ifdef USE_DSTRING
 #include "dstring.h"