Skip to content

Commit

Permalink
Clean up current file with uncaught exception crash
Browse files Browse the repository at this point in the history
  • Loading branch information
lucasdu2 committed Nov 26, 2024
1 parent 2b65646 commit 9734a70
Showing 1 changed file with 2 additions and 6 deletions.
8 changes: 2 additions & 6 deletions test/lucas-noob-work/clh_lock_clean.rav
Original file line number Diff line number Diff line change
Expand Up @@ -7,10 +7,6 @@ interface CLHLock {
module BoolType : Library.Type {
rep type T = Bool
}
module FracBool = Library.Frac[BoolType]

import FracBool.frac_chunk
ghost field agr: Agree

// ===========================================================================
// Section defining loc (just a flag for storing node "locked" state)
Expand Down Expand Up @@ -114,8 +110,6 @@ interface CLHLock {
if (!b) {
// TODO: think this through a bit more
fold acquired_node(node, r);
// NOTE: This line currently causes crash...won't dig further for now.
// fpu(pn, full_agr, frac_chunk(false, 1.0), frac_chunk(true, 1.0));
assert ln != pn;
// assert own(pn, full_agr, false, 1.0);
assert own(pn, locked, b, 0.5);
Expand Down Expand Up @@ -147,6 +141,8 @@ interface CLHLock {

unfold lock_inv(lk, r);
var pn: Ref := xchg(lk, ln);
// NOTE: When we added [b_disj := false], we get an uncaught exception error
// with some stack trace.
fold queued_loc(ln, r) [b_disj := false];
fold lock_inv(lk, r);

Expand Down

0 comments on commit 9734a70

Please sign in to comment.