Unhandled experimental intrinsics crash SMACK

[keram88]

Hello,

The following program causes unhandled intrinsic instructions to be emitted by Clang in LLVM:

int main() {
#pragma STDC FENV_ACCESS ON
  2.0f*1.0f;
}

(The FENV_ACCESS directive is meant to inhibit the ability of the optimizer's ability to optimize code related to accessing the floating point environment, such as rounding and exceptions).
This program produces the following unhandled intrinsic instruction: @llvm.experimental.constrained.fdiv.f32. However, there are more related instructions which also crash SMACK of the form @llvm.experimental.constrained.*. For instance, adding 2*1.0f produces these intrinsic instructions: @llvm.experimental.constrained.sitofp.f32.i32 and @llvm.experimental.constrained.fmul.f32.

A full list can be found here: https://llvm.org/docs/LangRef.html#constrained-floating-point-intrinsics

Since smack doesn't currently model floating point exceptions, we should probably raise a warning that these instructions are not supported and the verification could be unsound.

Thanks