Shaobo
Shaobo
> Why does it matter to SMACK what `long double` is in C? > LLVM has `x86_fp80` type, and hopefully that is what we use in our source code to...
> I agree with your point (2) above. My follow-up question is - do we have any regressions or are there any SVCOMP benchmarks that use `x86_fp80`? No, I think...
Just a follow-up on this issue: currently we provide warnings when unsoundness occurs.
Ok, this feature does not make sense because a verification of a Rust program actually involves compiling C programs. It only makes sense when we fix the compilation flags of...
I was wondering if it's still valid to assume that undefined values should hold the same value. I couldn't find any references now and intuitively they should be distinct.
We create a global variable for undefined values of a type.
Hi @hernanponcedeleon I assume the code fragment you attached is before the optimization passes applied by SMACK, some of which cannot preserve debug information. For example, we use the `mem2reg`...
> I see. So what are the trade-offs here? > I would guess it should be pretty easy to implement such a pass. > What are we losing when compared...
> Thanks @shaobo-he for your clarification above. > So what is the status of this? Could we steal SeaHorn pass for this? For my current use case, I don't need...
> What is happening with this one? Is it ready? I forgot. It's ready but it caused false alarms in SV-COMP benchmarks. I don't think the false alarms are a...