Re: [Xen-devel] [PATCH] coverity: Store the modelling file in the source tree.

[Tim Deegan <tim@xxxxxxx>]

At 15:29 +0000 on 04 Dec (1386167363), Andrew Cooper wrote:
> Signed-off-by: Andrew Cooper <andrew.cooper3@xxxxxxxxxx>
> CC: Keir Fraser <keir@xxxxxxx>
> CC: Jan Beulich <JBeulich@xxxxxxxx>
> CC: Tim Deegan <tim@xxxxxxx>
> CC: Ian Campbell <Ian.Campbell@xxxxxxxxxx>
> CC: Ian Jackson <Ian.Jackson@xxxxxxxxxxxxx>
> ---
>  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.
> + */

This is copied from the cpython model file, AFAICT.  Have you checked that
their license allows us to include it in Xen?  We might have to include
their copyright, BSD-style.

Tim.

> +
> +/* 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
> 

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