Skip to content

Not defining USE_DSTRING breaks cbmc #1837

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
romainbrenguier opened this issue Feb 14, 2018 · 1 comment
Closed

Not defining USE_DSTRING breaks cbmc #1837

romainbrenguier opened this issue Feb 14, 2018 · 1 comment

Comments

@romainbrenguier
Copy link
Contributor

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
@tautschnig
Copy link
Collaborator

tautschnig commented Feb 14, 2018

Just a few notes until time for a proper fix becomes available:

  1. expr_listt has a very small number of users and should be declared locally rather than imposing the list header on each and every file.
  2. "std_types.h" needs #include <unordered_map> (since 3f1fd64).

And then a lot more fixes are necessary ... working on it.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants