Zvonimir Rakamaric

My proposed fix is to keep track of stack allocation in a separate map. So instead of having just $Alloc we should probably have $HeapAlloc and $StackAlloc maps. Thoughts @michael-emmi...

Bumping this up since I would like to fix it since I think it might simplify some of our memory models. @michael-emmi I thought about your comment above. I am...

Can we fix this somehow?

Sorry, but how would moving procedures into separate files help? Also, for large projects we would be generating hundreds of such files. So even if this would help, I think...

I think it would be good to clarify what Corral exactly does in the presence of annotations. Clearly it does use pre- and post-conditions during verification (at least at call...

Another thing to note - we have been working on adding symbooglix as another backend verifier option. It is probably unlikely that whatever strategy we come up with here for...

Ok, we should do something about this. I had another thought recently related to this. Basically, our back-ends are not totally compatible, and will probably never be. For example, Boogie...

First of all, we should add a better error message if the top-level procedure is not found. I can do that. Now, how do you suggest we go about fixing...

SMACK has prototypical support for C++. I am not quite sure what exactly is the problem you are experiencing. Could you attach a small example here to help you out?

I don't quite understand this issue. Are you saying we are injecting checks even when overflow checking is not enabled in the command line?