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.
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.
Hello,
The following program causes unhandled intrinsic instructions to be emitted by Clang in LLVM:
(The
FENV_ACCESSdirective 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, adding2*1.0fproduces these intrinsic instructions:@llvm.experimental.constrained.sitofp.f32.i32and@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