<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><br><div><div>On May 9, 2011, at 4:38 PM, Rui Paulo wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><span class="Apple-style-span" style="border-collapse: separate; font-family: Helvetica; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; -webkit-text-decorations-in-effect: none; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; font-size: medium; ">Hi,<br><br>On May 9, 2011, at 4:09 PM, Ted Kremenek wrote:<br><br><blockquote type="cite">Hi Rui,<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">Two comments/questions:<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">1) Please do not use tabs. Please only use spaces (to follow LLVM coding conventions).<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">2) What is the role of lockHistory?<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">From what I can tell, lockHistory is trying to record information about events along a path, but it is doing so using state in the checker object. This isn't the right approach. Because the checker can be used to explore multiple paths in any arbitrary order, all checker state needs to be in GRState. Think of checkers as memory-less objects that cause state transitions in the GRState. Checkers can have state, but they are usually used to memoize computation. Any checker state for tracking the evolution of a bug along a specific path needs to be encoded in a GRState directly (and then ideally removed when it is no longer needed).<br></blockquote><br><br>Oh, right. The role of lockHistory is to track all the locks that we haven't yet unlocked. The current "state" also does this, but I don't think it keeps an order. I'll have to investigate further. It would be great if I didn't need to add anything to GRState. I'll also work on the test cases on my next opportunity.</span></blockquote></div><br><div>You can possibly use an ImmutableList to track lockset ordering (if ordering matters), and use the ImmutableList as the lockset data in GRState.</div></body></html>