declare mutex mutexdeclare rwlocks rwlock

これらのサブコマンドは (この後の declare root とともに)、主に、サポートするハーネスなしで、ライブラリを解析する際に使用されます。サブコマンド declare mutex と declare rwlocks は、特定された名前の相互排他ロックおよび読み取り側/書き込み側ロックを生成します。これらの名前は、その後の assert サブコマンドで利用されます。