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

[Andrew Cooper <andrew.cooper3@citrix.com>]

On 04/12/13 15:37, Tim Deegan wrote:
> At 15:29 +0000 on 04 Dec (1386167363), 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>
>> ---
>>  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.

Hmm - I knew I had forgotten something.

As for Python licensing, it is a little complicated.

>From their own licence file, their coverity modelling file is
"GPL-compatible", with the qualification of

(1) GPL-compatible doesn't mean that we're distributing Python under
    the GPL.  All Python licenses, unlike the GPL, let you distribute
    a modified version without making your changes open source.  The
    GPL-compatible licenses make it possible to combine Python with
    other software that is released under the GPL; the others don't.


In addition, it was only the header which was copied, being by far and
away the best and concise description of what a modelling file is and
how it works.

>From my reading of this, we are ok.

It might be reasonable to include a note saying that we used the cpython
modelling file as a reference (even Coverity themselves recommend it as
a reference), but that all content is Xen specific?

~Andrew

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