tools/checkers/vcc.h

   1 /*
   2  * Copyright (c) 2010 Martin Decky
   3  * All rights reserved.
   4  *
   5  * Redistribution and use in source and binary forms, with or without
   6  * modification, are permitted provided that the following conditions
   7  * are met:
   8  *
   9  * - Redistributions of source code must retain the above copyright
  10  *   notice, this list of conditions and the following disclaimer.
  11  * - Redistributions in binary form must reproduce the above copyright
  12  *   notice, this list of conditions and the following disclaimer in the
  13  *   documentation and/or other materials provided with the distribution.
  14  * - The name of the author may not be used to endorse or promote products
  15  *   derived from this software without specific prior written permission.
  16  *
  17  * THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR
  18  * IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
  19  * OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
  20  * IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT,
  21  * INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
  22  * NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
  23  * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
  24  * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
  25  * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
  26  * THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  27  */
  28
  29 /** @file
  30  *
  31  * VCC specifications tight to the HelenOS-specific annotations.
  32  *
  33  */
  34
  35 #ifndef HELENOS_VCC_H_
  36 #define HELENOS_VCC_H_
  37
  38 typedef _Bool bool;
  39
  40 #define __concat_identifiers_str(a, b)  a ## b
  41 #define __concat_identifiers(a, b)      __concat_identifiers_str(a, b)
  42
  43 #define __specification_attr(key, value) \
  44         __declspec(System.Diagnostics.Contracts.CodeContract.StringVccAttr, \
  45             key, value)
  46
  47 #define __specification_type(name) \
  48         __specification( \
  49                 typedef struct __concat_identifiers(_vcc_math_type_, name) { \
  50                         char _vcc_marker_for_math_type; \
  51                 } __concat_identifiers(\, name); \
  52         )
  53
  54 __specification(typedef void * \object;)
  55 __specification(typedef __int64 \integer;)
  56 __specification(typedef unsigned __int64 \size_t;)
  57
  58 __specification_type(objset)
  59
  60 __specification(struct \TypeState {
  61         __specification(ghost \integer \claim_count;)
  62         __specification(ghost bool \consistent;)
  63         __specification(ghost \objset \owns;)
  64         __specification(ghost \object \owner;)
  65         __specification(ghost bool \valid;)
  66 };)
  67
  68 __specification(bool \extent_mutable(\object);)
  69 __specification(\objset \extent(\object);)
  70 __specification(\objset \array_range(\object, \size_t);)
  71 __specification(bool \mutable_array(\object, \size_t);)
  72
  73 #endif
  74
  75 /** @}
  76  */