CBMC 5.93.0 cannot be built on non-Intel platforms

[lzaoral]

Due to the change in c1f9237, CBMC now cannot be compiled for aarch64, ppc64le and s390x targets which considerably complicates the ongoing package update in Fedora.

\cc: @vmihalko

[lzaoral]

Compilation error:

/builddir/build/BUILD/cbmc-cbmc-5.93.0/src/memory-analyzer/gdb_api.cpp:316:4: error: #error malloc calling conventions not know for current platform
  316 | #  error malloc calling conventions not know for current platform
      |    ^~~~~
/builddir/build/BUILD/cbmc-cbmc-5.93.0/src/memory-analyzer/gdb_api.cpp: In member function ‘void gdb_apit::collect_malloc_calls()’:
/builddir/build/BUILD/cbmc-cbmc-5.93.0/src/memory-analyzer/gdb_api.cpp:324:3: error: ‘record’ was not declared in this scope
  324 |   record = get_most_recent_record("*stopped");
      |   ^~~~~~
/builddir/build/BUILD/cbmc-cbmc-5.93.0/src/memory-analyzer/gdb_api.cpp:342:50: error: ‘allocated_size’ was not declared in this scope; did you mean ‘allocated_memory’?
  342 |   allocated_memory[get_register_value(record)] = allocated_size;
      |                                                  ^~~~~~~~~~~~~~
      |                                                  allocated_memory

[tautschnig]

Assuming https://src.fedoraproject.org/rpms/cbmc/blob/rawhide/f/cbmc.spec is the current state of play for Fedora it seems you are using CMake? Either way, though, I think we've made a mess of your config options and need to fix this so that WITH_MEMORY_ANALYZER can be set to off/zero and then really disable building that piece of code. That said: would you, on the Fedora side, be able to selectively set this to "off" for some architectures?

[lzaoral]

The current WIP spec is here: https://src.fedoraproject.org/rpms/cbmc/pull-request/3

That said, setting WITH_MEMORY_ANALYZER to OFF is definitely possible in the spec file and I'll do that right away. However, this should still be fixed in your upstream CMake configurations because it affects anyone who wants to build CBMC from source on a non-intel architecture.

[lzaoral]

Actaully, that won't work out-of-the-box either, because this condition will always evaluate to TRUE on any Linux platform:

cbmc/src/CMakeLists.txt

Lines 125 to 127 in c864ba9

	if((NOT WIN32 AND NOT APPLE) OR WITH_MEMORY_ANALYZER)
	add_subdirectory(memory-analyzer)
	endif()

[tautschnig]

Actaully, that won't work out-of-the-box either, because this condition will always evaluate to TRUE on any Linux platform:

Ack, that's why I said that we have made a mess of our config options. Will work on a fix.

[NlightNFotis]

Ping @esteffin as that may be of interest to him as well.

[tautschnig]

With apologies for the delay: @lzaoral , would you mind adding the patch from #7958 to your spec file to confirm this does the trick?

[lzaoral]

Thanks for the patch @tautschnig. I've already have applied something similar myself last week: https://src.fedoraproject.org/rpms/cbmc/blob/1636edb0d31b2d22dea4805efea0f700eda21459/f/cbmc-f40-fix-build.patch#_26

Right now, the package update is stuck on a crash reported in #7866 which has not received any response in more than 6 weeks.