Unhandled LLVM intrinsic generated from math.c

[keram88]

In the function fmodf there is a call to a Smack defined copysignf function. However, Clang generates a call to the llvm.copysign.f32 intrinsic instead. This is an issue because Smack doesn't currently model this intrinsic. There are two issues here:

• Why is Clang replacing this function?, and
• Smack should add support for this family of intrinsics

[keram88]

This program produces this intrinsic:

#include "smack.h"
#include <math.h>

int main() {
  double f = __VERIFIER_nondet_double();
  __VERIFIER_assume(!isnan(f));
  __VERIFIER_assume(0.0 < f);
  __VERIFIER_assume(isfinite(f));
  double z = fmodf(f, 2.0);
  __VERIFIER_assert(z <= 2.0);
}