Support suppressions used by UndefinedBehaviour Sanitizer

[ligurio]

CBMC has a mechanism for suppressing some checks inline using pragma directives:

#pragma CPROVER check push
#pragma CPROVER check disable "signed-overflow"
/* This addition will not trigger a signed overflow check. */
int c = a + b;
#pragma CPROVER check pop

UBsan is a popular sanitizer, and it has a way to suppressing checks using attributes ¹. The __attribute__((no_sanitize("undefined"))) function attribute is a compiler-specific mechanism used to disable UndefinedBehaviorSanitizer (UBSan) checks for a specific function.

Disable a specific check (nonnull-attribute):

static LJ_AINLINE char *lj_buf_wmem(char *p, const void *q, MSize len)
  __attribute__((no_sanitize("nonnull-attribute")));

Disable all checks:

#if defined(__clang__) || defined(__GNUC__)
__attribute__((no_sanitize("undefined")))
#endif
void deliberately_unsafe_function(int a, int b) {
  /* UBSan checks are disabled inside this function. */
  int c = a + b;
}

It's not very convenient to have different mechanisms for the different tools (UBSan and CBMC).

Footnotes

1. https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html#disabling-instrumentation-with-attribute-no-sanitize-undefined ↩