Boogie error: missing closing brace

The attached file results in the Boogie error stdin.bpl(4261,3): error: "}" expected Chalice (hg id -nibt): 61af32ca9b60+ 483+ default tip Boogie: 2.2.30705.1126

Id #4 | Release: None | Updated: Jun 19, 2013 at 9:15 AM by mschwerhoff | Created: Jun 19, 2013 at 9:15 AM by mschwerhoff

Boogie error when scaling read permissions

The Chalice program class Test { predicate P { rd(mu) } method test2() requires P requires unfolding rd(P) in true {} } results in the Boogie error stdin.bpl(454,52): Error: invalid argument...

Id #3 | Release: None | Updated: Jun 19, 2013 at 9:10 AM by mschwerhoff | Created: Jun 19, 2013 at 9:10 AM by mschwerhoff

Type-checker does not detect invalid permission scaling

The type-checker of Chalice should detect if counting permissions are attempted to be scaled (which is not allowed). At the moment, only in the translation phase this issue is recognized, which mak...

Id #2 | Release: None | Updated: Feb 15, 2013 at 4:44 PM by stefanheule | Created: Feb 15, 2013 at 4:44 PM by stefanheule

  • 1-3 of 3 Work Items
    • Previous
    • 1
    • Next
    • Showing
    • All
    • Work Items