[Xen-devel] [Patch v3] coverity: Store the modelling file in the source tree.

[Andrew Cooper <andrew.cooper3@xxxxxxxxxx>]

Signed-off-by: Andrew Cooper <andrew.cooper3@xxxxxxxxxx>
CC: Keir Fraser <keir@xxxxxxx>
CC: Jan Beulich <JBeulich@xxxxxxxx>
Acked-by: Tim Deegan <tim@xxxxxxx>
CC: Ian Campbell <Ian.Campbell@xxxxxxxxxx>
CC: Ian Jackson <Ian.Jackson@xxxxxxxxxxxxx>

---

Changes in v3:
 * Do not manually align the pointer for unmap_domain_page().  We should weed
   out the bad code in due course, so leave the errors visible.

Changes in v2:
 * Supply the PSF copyright statement, and an acknowledgement that their file
   was used as an example for ours, but that all content is Xen specific.
---
 misc/coverity_model.c |   74 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 74 insertions(+)
 create mode 100644 misc/coverity_model.c

diff --git a/misc/coverity_model.c b/misc/coverity_model.c
new file mode 100644
index 0000000..22cc32a
--- /dev/null
+++ b/misc/coverity_model.c
@@ -0,0 +1,74 @@
+/* Coverity Scan model
+ *
+ * This is a modeling file for Coverity Scan. Modeling helps to avoid false
+ * positives.
+ *
+ * - A model file can't import any header files.
+ * - Therefore only some built-in primitives like int, char and void are
+ *   available but not NULL etc.
+ * - Modeling doesn't need full structs and typedefs. Rudimentary structs
+ *   and similar types are sufficient.
+ * - An uninitialized local pointer is not an error. It signifies that the
+ *   variable could be either NULL or have some data.
+ *
+ * Coverity Scan doesn't pick up modifications automatically. The model file
+ * must be uploaded by an admin in the analysis.
+ *
+ * Copyright (c) 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010,
+ * 2011, 2012, 2013 Python Software Foundation; All Rights Reserved
+ *
+ * The Xen Coverity Scan modelling file used the cpython modelling file as a
+ * reference to get started (suggested by Coverty Scan themselves as a good
+ * example), but all content is Xen specific.
+ */
+
+/* Definitions */
+#define NULL (void *)0
+#define PAGE_SIZE 4096UL
+#define PAGE_MASK (~(PAGE_SIZE-1))
+
+#define assert(cond) /* empty */
+#define page_to_mfn(p) (unsigned long)(p)
+
+struct page_info {};
+
+/*
+ * map_domain_page() takes an existing domain page and possibly maps it into
+ * the Xen pagetables, to allow for direct access.  Model this as a memory
+ * allocation of exactly 1 page.
+ *
+ * map_domain_page() never fails (It will BUG() before returning NULL), and
+ * will only ever return page aligned addresses.
+ */
+void *map_domain_page(unsigned long mfn)
+{
+    void *p = __coverity_alloc__(PAGE_SIZE);
+
+    assert(p != NULL);
+    assert((p & ~PAGE_MASK) == 0);
+
+    return p;
+}
+
+void *__map_domain_page(struct page_info *page)
+{
+    return map_domain_page(page_to_mfn(page));
+}
+
+/*
+ * unmap_domain_page() will unmap a page.  Model it as a free().
+ */
+void unmap_domain_page(const void *va)
+{
+    __coverity_free__(v);
+}
+
+/*
+ * Local variables:
+ * mode: C
+ * c-file-style: "BSD"
+ * c-basic-offset: 4
+ * tab-width: 4
+ * indent-tabs-mode: nil
+ * End:
+ */
-- 
1.7.10.4


_______________________________________________
Xen-devel mailing list
Xen-devel@xxxxxxxxxxxxx
http://lists.xen.org/xen-devel