coverity: Store the modelling file in the source tree.

Signed-off-by: Andrew Cooper <andrew.cooper3@citrix.com>
CC: Coverity Team <coverity@xenproject.org>
Acked-by: Ian Campbell <ian.campbell@citrix.com>
This commit is contained in:
Andrew Cooper authored and Ian Campbell committed 2014-03-12 14:14:59 +00:00
1 parent 015d6ed025
commit 25e3f24b6d
1 file changed
+131
+131
View File
@@ -0,0 +1,131 @@
/* Coverity Scan model
*
* This is a modelling file for Coverity Scan. Modelling 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.
* - Modelling doesn't need full structs and typedefs. Rudimentary structs
* and similar types are sufficient.
* - An uninitialised 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.
*
* 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.
*
* Copyright (c) 2013-2014 Citrix Systems Ltd; All Right Reserved
*
* Based on:
* http://hg.python.org/cpython/file/tip/Misc/coverity_model.c
* Copyright (c) 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010,
* 2011, 2012, 2013 Python Software Foundation; All Rights Reserved
*
*/
/*
* Useful references:
* https://scan.coverity.com/models
*/
/* Definitions */
#define NULL (void *)0
#define PAGE_SIZE 4096UL
#define PAGE_MASK (~(PAGE_SIZE-1))
#define assert(cond) /* empty */
struct page_info {};
struct pthread_mutex_t {};
struct libxl__ctx
{
struct pthread_mutex_t lock;
};
typedef struct libxl__ctx libxl_ctx;
/*
* Xen malloc. Behaves exactly like regular malloc(), except it also contains
* an alignment parameter.
*
* TODO: work out how to correctly model bad alignments as errors.
*/
void *_xmalloc(unsigned long size, unsigned long align)
{
int has_memory;
__coverity_negative_sink__(size);
__coverity_negative_sink__(align);
if ( has_memory )
return __coverity_alloc__(size);
else
return NULL;
}
/*
* Xen free. Frees a pointer allocated by _xmalloc().
*/
void xfree(void *va)
{
__coverity_free__(va);
}
/*
* 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)
*
* TODO: work out how to correctly model the behaviour that this function will
* only ever return page aligned pointers.
*/
void *map_domain_page(unsigned long mfn)
{
return __coverity_alloc__(PAGE_SIZE);
}
/*
* unmap_domain_page() will unmap a page. Model it as a free().
*/
void unmap_domain_page(const void *va)
{
__coverity_free__(va);
}
/*
* Coverity appears not to understand that errx() unconditionally exits.
*/
void errx(int, const char*, ...)
{
__coverity_panic__();
}
/*
* Coverity doesn't appear to be certain that the libxl ctx->lock is recursive.
*/
void libxl__ctx_lock(libxl_ctx *ctx)
{
__coverity_recursive_lock_acquire__(&ctx->lock);
}
void libxl__ctx_unlock(libxl_ctx *ctx)
{
__coverity_recursive_lock_release__(&ctx->lock);
}
/*
* Local variables:
* mode: C
* c-file-style: "BSD"
* c-basic-offset: 4
* tab-width: 4
* indent-tabs-mode: nil
* End:
*/
Reference in new issue
Block a user
Blocking a user prevents them from interacting with repositories, such as opening or commenting on pull requests or issues. Learn more about blocking a user.