+// Report a detected internal inconsistency.
+void
+__warn_internalerror(int lineno, const char *fname)
+{
+ dprintf(1, "WARNING - internal error detected at %s:%d!\n"
+ , fname, lineno);
+}
+
+// Report on an allocation failure.
+void
+__warn_noalloc(int lineno, const char *fname)
+{
+ dprintf(1, "WARNING - Unable to allocate resource at %s:%d!\n"
+ , fname, lineno);
+}
+
+// Report on a timeout exceeded.
+void
+__warn_timeout(int lineno, const char *fname)
+{
+ dprintf(1, "WARNING - Timeout at %s:%d!\n", fname, lineno);
+}
+