Skip to content

Build fails on Apple Silicon #7922

Closed
@esteffin

Description

@esteffin

CProver build fails when executing the memory-analyzer subtask on Apple Silicon (using CMake).

Specifically the error is:

/Users/esteffin/git/cbmc/src/memory-analyzer/gdb_api.cpp:316:4: error: malloc calling conventions not know for current platform
#  error malloc calling conventions not know for current platform
   ^
/Users/esteffin/git/cbmc/src/memory-analyzer/gdb_api.cpp:324:3: error: use of undeclared identifier 'record'
  record = get_most_recent_record("*stopped");
  ^
/Users/esteffin/git/cbmc/src/memory-analyzer/gdb_api.cpp:325:46: error: use of undeclared identifier 'record'
  auto frame_content = get_value_from_record(record, "frame");
                                             ^
/Users/esteffin/git/cbmc/src/memory-analyzer/gdb_api.cpp:336:5: error: use of undeclared identifier 'record'
    record = get_most_recent_record("*stopped");
    ^
/Users/esteffin/git/cbmc/src/memory-analyzer/gdb_api.cpp:341:3: error: use of undeclared identifier 'record'
  record = get_most_recent_record("^done", true);
  ^
/Users/esteffin/git/cbmc/src/memory-analyzer/gdb_api.cpp:342:39: error: use of undeclared identifier 'record'
  allocated_memory[get_register_value(record)] = allocated_size;
                                      ^
/Users/esteffin/git/cbmc/src/memory-analyzer/gdb_api.cpp:342:50: error: use of undeclared identifier 'allocated_size'
  allocated_memory[get_register_value(record)] = allocated_size;

The offending changes have been introduced in c1f9237e36d09d47eb58f2c191b5edf2f9bc1a7c and part of PR (#7756) at c1f9237#diff-528c73e43b559ab716b320cc9945a0d95c99ea6b5de697f0e0e6910644775cfdR290.

Specifically in src/memory-analyzer/gdb_api.cpp:290 the variable record and allocated_size declaration have been guarded by __x86_64__ and __i386__, so on Apple Silicon (that is not __x86_64__ nor __i386__) the build fail at line 316 because of # error malloc calling conventions not know for current platform and subsequently with undefined variables.

CBMC version: develop
Operating system: MacOS Ventura on Apple Silicon
Exact command line resulting in the issue: cmake .. and then make or make memory-analyzer
What behaviour did you expect: successful build
What happened instead: build failure

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