Mark S. Baranowski
Mark S. Baranowski
Hello, I have been exploring some new use cases for SMACK and encountered a need to create some uninterpreted functions at the C level, such as the following: ```c float...
Hello, The following program causes unhandled intrinsic instructions to be emitted by Clang in LLVM: ```C int main() { #pragma STDC FENV_ACCESS ON 2.0f*1.0f; } ``` (The `FENV_ACCESS` directive is...
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...
The binary package for Z3 we use seems to be linked to a newer libm that is not available in 18.04. A possible solution is to switch the default Ubuntu...
A map for the dark, deep mines within Gelpia. Adventurous users will want to avoid the Balrog at any cost!
We need to show the expression where division by zero is detected.
The update thread in the cooperative solver will most likely never see the termination signal as it will be waiting at one of the two barriers. Find a way to...
It appears clang translates calls to the `copysign` functions to the corresponding LLVM copysign intrinsics (such as `@llvm.copysign.f32`). This leads to failures when using the copysign functions and the fmod...