You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Commenting out #define USE_DSTRING means cbmc does not compile.
The possibility of commenting this does not seem to be used, and has not been tested for some time.
We should determine whether it's useful to have this possibility and if yes fix the compilation problems.
[ 5%] Building CXX object lib/cbmc/src/util/CMakeFiles/util.dir/array_name.cpp.o
In file included from cbmc/src/util/std_types.h:19:0,
from cbmc/src/util/arith_tools.cpp:15:
cbmc/src/util/expr.h:181:14: error: ‘list’ in namespace ‘std’ does not name a template type
typedef std::list<exprt> expr_listt;
^
In file included from cbmc/src/util/arith_tools.cpp:15:0:
cbmc/src/util/std_types.h:903:10: error: ‘unordered_map’ in namespace ‘std’ does not name a template type
std::unordered_map<irep_idt, std::size_t, irep_id_hash> parameter_indicest;
^
/home/romain/git/test-gen/lib/cbmc/src/util/std_types.h:906:3: error: ‘parameter_indicest’ does not name a type
parameter_indicest parameter_indices() const
^
cbmc/src/util/CMakeFiles/util.dir/build.make:62: recipe for target 'cbmc/src/util/CMakeFiles/util.dir/arith_tools.cpp.o' failed
make[3]: *** [lib/cbmc/src/util/CMakeFiles/util.dir/arith_tools.cpp.o] Error 1
make[3]: *** Waiting for unfinished jobs....
In file included from cbmc/src/util/array_name.cpp:14:0:
cbmc/src/util/expr.h:181:14: error: ‘list’ in namespace ‘std’ does not name a template type
typedef std::list<exprt> expr_listt;
^
In file included from cbmc/src/util/std_expr.h:21:0,
from bmc/src/util/ssa_expr.h:13,
from cbmc/src/util/array_name.cpp:17:
cbmc/src/util/std_types.h:903:10: error: ‘unordered_map’ in namespace ‘std’ does not name a template type
std::unordered_map<irep_idt, std::size_t, irep_id_hash> parameter_indicest;
^
cbmc/src/util/std_types.h:906:3: error: ‘parameter_indicest’ does not name a type
parameter_indicest parameter_indices() const
^
lib/cbmc/src/util/CMakeFiles/util.dir/build.make:86: recipe for target 'lib/cbmc/src/util/CMakeFiles/util.dir/array_name.cpp.o' failed
make[3]: *** [lib/cbmc/src/util/CMakeFiles/util.dir/array_name.cpp.o] Error 1
CMakeFiles/Makefile2:1307: recipe for target 'lib/cbmc/src/util/CMakeFiles/util.dir/all' failed
make[2]: *** [lib/cbmc/src/util/CMakeFiles/util.dir/all] Error 2
CMakeFiles/Makefile2:1814: recipe for target 'lib/cbmc/src/cbmc/CMakeFiles/cbmc.dir/rule' failed
make[1]: *** [lib/cbmc/src/cbmc/CMakeFiles/cbmc.dir/rule] Error 2
Makefile:532: recipe for target 'cbmc' failed
make: *** [cbmc] Error 2
The text was updated successfully, but these errors were encountered:
Commenting out
#define USE_DSTRING
means cbmc does not compile.The possibility of commenting this does not seem to be used, and has not been tested for some time.
We should determine whether it's useful to have this possibility and if yes fix the compilation problems.
The text was updated successfully, but these errors were encountered: