From: Andrew Cooper <andrew.cooper3@citrix.com>
To: Xen-devel <xen-devel@lists.xen.org>
Cc: Keir Fraser <keir@xen.org>,
Ian Campbell <Ian.Campbell@citrix.com>,
Andrew Cooper <andrew.cooper3@citrix.com>,
Ian Jackson <Ian.Jackson@eu.citrix.com>, Tim Deegan <tim@xen.org>,
Jan Beulich <JBeulich@suse.com>
Subject: [PATCH] coverity: Store the modelling file in the source tree.
Date: Wed, 4 Dec 2013 15:29:23 +0000 [thread overview]
Message-ID: <1386170963-8980-1-git-send-email-andrew.cooper3@citrix.com> (raw)
Signed-off-by: Andrew Cooper <andrew.cooper3@citrix.com>
CC: Keir Fraser <keir@xen.org>
CC: Jan Beulich <JBeulich@suse.com>
CC: Tim Deegan <tim@xen.org>
CC: Ian Campbell <Ian.Campbell@citrix.com>
CC: Ian Jackson <Ian.Jackson@eu.citrix.com>
---
misc/coverity_model.c | 70 +++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 70 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..2588adb
--- /dev/null
+++ b/misc/coverity_model.c
@@ -0,0 +1,70 @@
+/* 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 wchar_t, 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.
+ */
+
+/* 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 correctly unmap the page, given any virtual
+ * address inside the page.
+ */
+void unmap_domain_page(const void *va)
+{
+ const void *v = (const void*)((unsigned long)va & PAGE_MASK);
+
+ __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
next reply other threads:[~2013-12-04 15:29 UTC|newest]
Thread overview: 6+ messages / expand[flat|nested] mbox.gz Atom feed top
2013-12-04 15:29 Andrew Cooper [this message]
2013-12-04 15:37 ` [PATCH] coverity: Store the modelling file in the source tree Tim Deegan
2013-12-04 15:48 ` Andrew Cooper
2013-12-04 15:54 ` Tim Deegan
2013-12-04 16:11 ` David Vrabel
2013-12-04 16:33 ` Andrew Cooper
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=1386170963-8980-1-git-send-email-andrew.cooper3@citrix.com \
--to=andrew.cooper3@citrix.com \
--cc=Ian.Campbell@citrix.com \
--cc=Ian.Jackson@eu.citrix.com \
--cc=JBeulich@suse.com \
--cc=keir@xen.org \
--cc=tim@xen.org \
--cc=xen-devel@lists.xen.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).