bitcalc

The __SMACK_check_memory_leak() function asserts the value of $allocatedCounter to be 0. I don't understand why the unroll of the loop in strlen affects the memory leak assertion?

According to your explanation, I'd like to confirm with you a couple of things: 1. SMACK can only establish the loop termination fact after I set the unrolling number greater...

The 3rd item above is very useful to us. Could you revisit it? We want to prove some security properties hold reliably, a missing or unverified assertion in the code...

I've looked into the llvm2bpl.cpp file and noticed that the current implementation uses existing LLVM passes and SMACK passes to transform the initial LLVM bitcode. It is hard for me...

After playing more with LLVM-based versifiers, I've observed the point that they have the same problem. So I'm with you. For practical purpose, an easier alternative (than comparing the LLVM...

Since I'm new to Boogie, I'd like to venture out to give my thoughts on how to handle the internal structure of a C struct for the exercise purpose. For...

I happened to communicate with @zvonimir, and this is what we've said about the second issue. > @zvonimir > Your solution seems to be a step in the right direction....