Skip to content

Not defining USE_DSTRING breaks cbmc  #1837

Closed
@romainbrenguier

Description

@romainbrenguier

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

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions