Skip to content

discrepancy between cbmc and gcc/clang with structs with bitfields #8955

@GenericNerdyUsername

Description

@GenericNerdyUsername

The following code has its assertion succeed when compiled with gcc or clang (with a small amount of code prepended), but not with cbmc:

typedef struct {
  unsigned c : 1;
} inner_container_t;

struct container_t {
  inner_container_t inner_container;
  int i;
};

int main() {
  container_t container;
  container.inner_container.c = 1;
  __CPROVER_printf("before: %d\n", container.inner_container.c);

  *(&(&container) -> i) = 0;

  __CPROVER_printf("after: %d\n", container.inner_container.c);
  __CPROVER_assert(container.inner_container.c, "");
  return 0;
}

The prepended code is

#include <stdio.h>
#include <assert.h>

#define __CPROVER_printf printf

void __CPROVER_assert(bool good, const char* msg) {
  assert(good);
}

Removing the bitfield allows cbmc to succed, as does removing some of the pointer fuckery.

Am I missing something or is this a bug in cbmc?

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions