Issues that came up when verifying lclist

[nrp364]

Two issues:

1. See :

   raven/test/comparison/lclist.rav

   Line 95 in 56efd71

   proc create_buggy()

Procedure create_buggy should not verify, but it does! The command fold is_list(r, 0); in line 110 specifically should not pass because the heap has own(r.agr, Agree.agree(null) but the fold command requires own(r.agr, Agree.agree(l). There is no fpu that is possible here. I checked the Agreement RA, but didn't find anything obviously incorrect there.

2. See :

   raven/test/comparison/lclist.rav

   Line 66 in 56efd71

   // Below should work, instead we get an error:

Probably something going wrong/being prohibited by the mask analysis. Note that both modules NodeResource and LCLock have a lemma called exclusive, but I am explicitly calling the one for NodeResource.