[Ur] Almost 100% bug in request() algorithm

[Adam Chlipala]

Thanks for the patch!  I agree with your problem diagnosis and solution, 
and your patch is now pushed to the working repository.

As you can see, too much formal verification has made my brain mushy, so 
it needs to do proofs to detect bugs like this anymore. ;)

On 06/15/2014 05:15 PM, Sergey Mironov wrote:
> That is how I fixed the problem. I didn't check all the consequences
> of this fix.
>
> 2014-06-16 1:10 GMT+04:00 Sergey Mironov <grrwlf at gmail.com>:
>> Hi! I've found a bug while debugging my FFI code!
>>
>> Look at the request() from request.c. It contains the following pattern:
>>
>> [...]
>>
>> Note, that try_rollback() is executed _after_
>> uw_reset_keep_error_message(). It is an error because reset will
>> assign ctx->used_transactionals to 0 and prevent FFI cleanup handlers
>> from working! Let me suggest calling try_rollback() before reset.