Shaobo
Shaobo
This issue has been resolved: we model realloc as free-then-malloc.
> Has Mark's program been added to our regressions? No, SMACK reports an error for Mark's program as we don't model copying in realloc.
> Could we update the model to include copying as well? This might be very tricky since we have to keep track of the memory associated with the base pointer....
Thank you for the request. We have an option that enables LLVM's static loop unrolling pass, which unrolls a loop completely if it can determine the loop bound. This option...
Inspired by Facebook infer's `-- make` option, maybe we can add a similar option to SMACK such that SMACK can work on projects using `make` build system.
I would propose we remove the optimization in the `Div` function of `formula.py` and put it in the simplifier.
> I am not sure this is a premature optimization. Indeed we could raise an exception signaling the problem, but I would avoid the possibility of even creating a formula...
@zvonimir @michael-emmi @keram88, I think our documentations are very out-of-dated. I added some points about how we should update them. Any feedback? Btw, I should add Rust stuff into them,...
I think we shouldn't ignore them because I think we'd like to make the handling of undefined behaviors consistent (i.e., respect the common-sense compiler). For strict-aliasing violations, we simply assume...
> One potential fix is to keep track of everything that gets allocated via `alloca` instruction. Then, all such objects should be freed before every return. I wonder if this...