From 526206aabe017aa490ec8b5874399472fdf72351 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Sun, 17 Oct 2021 15:15:45 +1100
Subject: [PATCH] libsel4 idl: error conditions of SchedContext bind

Add error conditions for the lazy bind of SchedContexts to
notifications or TCBs (introduced in e18e32e28e).

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 libsel4/include/interfaces/sel4.xml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/libsel4/include/interfaces/sel4.xml b/libsel4/include/interfaces/sel4.xml
index c5956d25e..cd9cb04ea 100644
--- a/libsel4/include/interfaces/sel4.xml
+++ b/libsel4/include/interfaces/sel4.xml
@@ -1369,8 +1369,9 @@
                 a signal arrives, the passive thread will receive the scheduling context and possess it
                 until it waits on the notification object again.
 
-                This operation will fail if the scheduling context is already bound to a thread or
-                notification object.
+                This operation will fail for notification objects if the scheduling context is already
+                bound to a notification object, and for thread objects if the the scheduling context is
+                already bound to a thread.
             </brief>
             <description>
                 See <autoref label="sec:threads"/>
@@ -1381,7 +1382,7 @@
             <error name="seL4_IllegalOperation">
                 <description>
                     The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
-                    Or, <texttt text="_service"/> or <texttt text="cap"/> is already bound.
+                    Or, <texttt text="_service"/> or <texttt text="cap"/> is already bound to the same type of object.
                     Or, <texttt text="cap"/> is a TCB in the blocked state and <texttt text="_service"/> is not schedulable.
                 </description>
             </error>