Assertion `a.is_constant()' failed at value_set.cpp:804

[Anthonysdu]

#define PAGE_SIZE ((1) << XLAT_GRANULARITY_SIZE_SHIFT)

struct rmm_core_manifest {
  int a;
};

int main() {
  static unsigned char el3_rmm_shared_buffer[PAGE_SIZE]
      __attribute__((__aligned__(PAGE_SIZE)));
  static struct rmm_core_manifest *boot_manifest =
      (struct rmm_core_manifest *)el3_rmm_shared_buffer;

  return 0;
}

esbmc main.c -DXLAT_GRANULARITY_SIZE_SHIFT=7:

ESBMC version 7.5.0 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
Enabling --no-slice due to presence of --smt-during-symex
Parsing main.c
Converting
Generating GOTO Program
GOTO program creation time: 0.059s
GOTO program processing time: 0.000s
No solver specified; defaulting to Boolector
Starting Bounded Model Checking
esbmc: /home/runner/work/esbmc/esbmc/src/pointer-analysis/value_set.cpp:804: void value_sett::get_reference_set_rec(const expr2tc&, value_sett::object_mapt&) const: Assertion `a.is_constant()' failed.
Aborted (core dumped)

[fbrausse]

This should be relatively easy to resolve in the clang-c frontend: The alignment needs to be a compile-time constant. Maybe we're not using the right Clang API to obtain it.