Andrew Cooper
2013-Dec-04 16:58 UTC
[Patch v2] coverity: Store the modelling file in the source tree.
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> --- 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 | 77 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 77 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..2b39b3c --- /dev/null +++ b/misc/coverity_model.c @@ -0,0 +1,77 @@ +/* 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 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
Tim Deegan
2013-Dec-04 17:11 UTC
Re: [Patch v2] coverity: Store the modelling file in the source tree.
At 16:58 +0000 on 04 Dec (1386172702), Andrew Cooper wrote:> 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>Acked-by: Tim Deegan <tim@xen.org>