1 /* Coverity Scan model
2 *
3 * This is a modelling file for Coverity Scan. Modelling helps to avoid false
4 * positives.
5 *
6 * - A model file can't import any header files.
7 * - Therefore only some built-in primitives like int, char and void are
8 * available but not NULL etc.
9 * - Modelling doesn't need full structs and typedefs. Rudimentary structs
10 * and similar types are sufficient.
11 * - An uninitialised local pointer is not an error. It signifies that the
12 * variable could be either NULL or have some data.
13 *
14 * Coverity Scan doesn't pick up modifications automatically. The model file
15 * must be uploaded by an admin in the analysis.
16 *
17 * The Xen Coverity Scan modelling file used the cpython modelling file as a
18 * reference to get started (suggested by Coverty Scan themselves as a good
19 * example), but all content is Xen specific.
20 *
21 * Copyright (c) 2013-2014 Citrix Systems Ltd; All Right Reserved
22 *
23 * Based on:
24 * http://hg.python.org/cpython/file/tip/Misc/coverity_model.c
25 * Copyright (c) 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010,
26 * 2011, 2012, 2013 Python Software Foundation; All Rights Reserved
27 *
28 */
29
30 /*
31 * Useful references:
32 * https://scan.coverity.com/models
33 */
34
35 /* Definitions */
36 #define NULL (void *)0
37 #define PAGE_SIZE 4096UL
38 #define PAGE_MASK (~(PAGE_SIZE-1))
39
40 #define assert(cond) /* empty */
41
42 struct page_info {};
43 struct pthread_mutex_t {};
44
45 struct libxl__ctx
46 {
47 struct pthread_mutex_t lock;
48 };
49 typedef struct libxl__ctx libxl_ctx;
50
51 /*
52 * Xen malloc. Behaves exactly like regular malloc(), except it also contains
53 * an alignment parameter.
54 *
55 * TODO: work out how to correctly model bad alignments as errors.
56 */
_xmalloc(unsigned long size,unsigned long align)57 void *_xmalloc(unsigned long size, unsigned long align)
58 {
59 int has_memory;
60
61 __coverity_negative_sink__(size);
62 __coverity_negative_sink__(align);
63
64 if ( has_memory )
65 return __coverity_alloc__(size);
66 else
67 return NULL;
68 }
69
70 /*
71 * Xen free. Frees a pointer allocated by _xmalloc().
72 */
xfree(void * va)73 void xfree(void *va)
74 {
75 __coverity_free__(va);
76 }
77
78
79 /*
80 * map_domain_page() takes an existing domain page and possibly maps it into
81 * the Xen pagetables, to allow for direct access. Model this as a memory
82 * allocation of exactly 1 page.
83 *
84 * map_domain_page() never fails. (It will BUG() before returning NULL)
85 *
86 * TODO: work out how to correctly model the behaviour that this function will
87 * only ever return page aligned pointers.
88 */
map_domain_page(unsigned long mfn)89 void *map_domain_page(unsigned long mfn)
90 {
91 return __coverity_alloc__(PAGE_SIZE);
92 }
93
94 /*
95 * unmap_domain_page() will unmap a page. Model it as a free().
96 */
unmap_domain_page(const void * va)97 void unmap_domain_page(const void *va)
98 {
99 __coverity_free__(va);
100 }
101
102 /*
103 * Coverity appears not to understand that errx() unconditionally exits.
104 */
errx(int,const char *,...)105 void errx(int, const char*, ...)
106 {
107 __coverity_panic__();
108 }
109
110 /*
111 * Coverity doesn't appear to be certain that the libxl ctx->lock is recursive.
112 */
libxl__ctx_lock(libxl_ctx * ctx)113 void libxl__ctx_lock(libxl_ctx *ctx)
114 {
115 __coverity_recursive_lock_acquire__(&ctx->lock);
116 }
117
libxl__ctx_unlock(libxl_ctx * ctx)118 void libxl__ctx_unlock(libxl_ctx *ctx)
119 {
120 __coverity_recursive_lock_release__(&ctx->lock);
121 }
122
123 /*
124 * Coverity doesn't understand __builtin_unreachable(), which causes it to
125 * incorrectly find issues based on continuing execution along the false
126 * branch of an ASSERT().
127 */
__builtin_unreachable(void)128 void __builtin_unreachable(void)
129 {
130 __coverity_panic__();
131 }
132
133 /*
134 * Local variables:
135 * mode: C
136 * c-file-style: "BSD"
137 * c-basic-offset: 4
138 * tab-width: 4
139 * indent-tabs-mode: nil
140 * End:
141 */
142