Patchwork [Ada] Use assertion to verify representation invariant for lock status

login
register
mail settings
Submitter Arnaud Charlet
Date Aug. 31, 2011, 9:27 a.m.
Message ID <20110831092746.GA17824@adacore.com>
Download mbox | patch
Permalink /patch/112482/
State New
Headers show

Comments

Arnaud Charlet - Aug. 31, 2011, 9:27 a.m.
Replaced a comment about lock status with a proper assertion, and added a
comment to explain the representation invariant for the lock status.

Tested on x86_64-pc-linux-gnu, committed on trunk

2011-08-31  Matthew Heaney  <heaney@adacore.com>

	* a-rbtgbo.adb (Clear_Tree): Assert representation invariant for lock
	status.

Patch

Index: a-rbtgbo.adb
===================================================================
--- a-rbtgbo.adb	(revision 178368)
+++ a-rbtgbo.adb	(working copy)
@@ -59,15 +59,16 @@ 
            "attempt to tamper with cursors (container is busy)";
       end if;
 
+      --  The lock status (which monitors "element tampering") always implies
+      --  that the busy status (which monitors "cursor tampering") is set too;
+      --  this is a representation invariant. Thus if the busy bit is not set,
+      --  then the lock bit must not be set either.
+      pragma Assert (Tree.Lock = 0);
+
       Tree.First  := 0;
       Tree.Last   := 0;
       Tree.Root   := 0;
       Tree.Length := 0;
-
-      --  Why are the following commented out with no explanation ???
-      --  Tree.Busy
-      --  Tree.Lock
-
       Tree.Free   := -1;
    end Clear_Tree;