lock.c-explain.html from CQual at Krugle

Show lock.c-explain.html syntax highlighted


<html>
<body bgcolor="white">
<h2>Locking:  Small Example</h2>

<p>
The lower left pane contains the original program, and the lower right
pane contains the program with qualifier annotations.

<p>
In this example, the functions <tt>spin_lock</tt> and
<tt>spin_unlock</tt>, which contain magic assembly code (omitted), are
called to acquire and release a lock, respectively.  The main function
first acquires and then releases <tt>rtc_lock</tt>.

<p>
In the lower right pane we've added qualifiers <tt>$locked</tt> and
<tt>$unlocked</tt> indicating that <tt>spin_lock</tt> and
<tt>spin_unlock</tt> require their arguments be in the correct state.
We've also added <tt>change_type</tt> statements to capture the effect
of the assembly code.  The expression <tt>change_type(x, type)</tt> is
treated exactly like an assignment to <tt>x</tt>, except rather than
giving an expression for the right-hand side you only need to supply
the type of the right-hand side.  We also declare that in the initial
environment, <tt>rtc_lock</tt> is <tt>$unlocked</tt>.
</body>
</html>

See more files for this project here