seahorn/crab

g++-8:

elazarg opened this issue · 4 comments

g++-8 now warns about "writing to an object of non-trivially copyable type" using memcpy:

crab/install/include/crab/domains/graphs/adapt_sgraph.hpp:59:15: 
   error: ‘void* memcpy(void*, const void*, size_t)’
   writing to an object of non-trivially copyable type ‘class crab::AdaptSMap<long unsigned int>::elt_t’; 
   use copy-assignment or copy-initialization instead [-Werror=class-memaccess]
         memcpy(dense, o.dense, sizeof(elt_t)*sz);
         ~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

The warning is enabled automatically on -Wall.

I'm not sure if it helps to solve the problem but could you please try
memcpy(static_cast<void*>(dense), static_cast<void*>(o.dense), sizeof(elt_t)*sz)?

It silences the error. Also the following should be handled (either memcpy or realloc)
crab/install/include/crab/domains/graphs/util/Vec.h at 121, 148
crab/install/include/crab/domains/graphs/adapt_sgraph.hpp 274

Are you sure it doesn't mask a bug? It does seem strange to memcpy a non-trivially copyable data structure.

It's done in this way for efficiency reasons. The copied objects are supposed to be basic types so it should be fine. Vec.h assumes that the type of the vector element is re-allocable so it should be also fine.
However, it's true that this makes the code less general. For instance, all this code is used to represent weighted graphs. Right now, the weights must be basic types but I would like to have other types (e.g., ikos::z_number) so it has been on my TODO list for a while.

The compilation errors should be gone with commit 9e51d45
I created a new issue #22 related to this.