\begin{table}[t!]
\small
\begin{tabular}{|p{0.1in}|p{0.5in}|p{0.5in}|p{1.55in}|}
\hline
\hline
& {\bf Driver class} & {\bf Category} & {\bf Assertion}
\\
\hline
1 & PCI Net   & \codesm{probe} &
   Calls \codesm{register\_netdev} on success
   \\
\hline
2 & Net          & \codesm{open} &
   Calls \codesm{netif\_start\_queue} on success
   \\
\hline
3 & Net          & \codesm{close} &
   Calls \codesm{netif\_stop\_queue} on success
   \\
\hline
4 & Net          & \codesm{open} &
   Driver not already opened
   \\
\hline
5 & Net          & \codesm{tx} &
   The \codesm{dev->trans\_start} field is unchanged
   \\
\hline
6 & PCI Any      & N/A &
   Calls \codesm{pci\_\-disable\_\-device} only if
   \codesm{pci\_\-enable\_\-device} was
   successful
   \\
\hline
7 & PCI Net      & N/A &
   Calls \codesm{pci\_\-disable\_\-device} only if
   \codesm{unre\-gi\-ster\_\-netdev} was
   called or if \codesm{register\_\-netdev}
   failed
   \\
\hline
8 & PCI          & N/A &
   Calls \codesm{pci\_register\_driver} in the
   driver's \codesm{init\_module} routine.
   \\
\hline
9 & PCI          & N/A &
   Calls \codesm{pci\_unregister\_driver in the
   driver's \codesm{cleanup\_module} routine.
   \\
\hline
12 & All          & Object tracking &
   All allocated memory resources are
   freed appropriately.  (Supports 12 pairs
   of allocator/deallocator functions).
   \\
\hline
13 & All          & Execution context &
   Functions use the appropriate
   \codesm{gfp\_t} memory allocation flags
   according to the execution context.
   \\
\hline
14 & All         & Execution context &
   The driver does not allocate
   resources along an exection path invokable
   by an unprivileged user.
   \\
\hline
15 & All         & Lock tracking &
   All acquired locks are released.
   Dymanically-allocated locks are
   properly initialized first.  (Supports 20 pairs
   of lock/unlock functions).
   \\
\hline
16 & All         & \codesm{copy\_to/from\_user} &
   The buffer into which \codesm{copy\_from\_user}
   copies is large enough to hold the data.
   \\
\hline
17 & PCI net     & \codesm{ioctl} &
   The driver's \codesm{ioctl} routine does not
   perform redundant permission checks.
   \\
\hline


\hline
\end{tabular}
\caption{\small \bf \Arch\ can detect a variety of driver bugs that would be
  difficult using grep, static analysis, or simply executing the driver.}
\label{fig:table-test}
\vspace{-0.1in}
\end{table}
