Changeset 33c4f72 in mainline


Ignore:
Timestamp:
2010-06-25T13:38:30Z (14 years ago)
Author:
Martin Decky <martin@…>
Branches:
lfn, master, serial, ticket/834-toolchain-update, topic/msim-upgrade, topic/simplify-dev-export
Children:
fc81981
Parents:
09a0bd4a
Message:

improve annotations
move to the newest VCC syntax
use VCC specifications as a separate vcc.h header

Files:
1 added
4 edited

Legend:

Unmodified
Added
Removed

  • kernel/arch/abs32le/include/atomic.h

    r09a0bd4a r33c4f72  
    4242
    4343ATOMIC static inline void atomic_inc(atomic_t *val)
     44    WRITES(&val->count)
     45    REQUIRES_EXTENT_MUTABLE(val)
    4446    REQUIRES(val->count < ATOMIC_COUNT_MAX)
    4547{
    … …  
    5153
    5254ATOMIC static inline void atomic_dec(atomic_t *val)
     55    WRITES(&val->count)
     56    REQUIRES_EXTENT_MUTABLE(val)
    5357    REQUIRES(val->count > ATOMIC_COUNT_MIN)
    5458{
    … …  
    6064
    6165ATOMIC static inline atomic_count_t atomic_postinc(atomic_t *val)
     66    WRITES(&val->count)
     67    REQUIRES_EXTENT_MUTABLE(val)
    6268    REQUIRES(val->count < ATOMIC_COUNT_MAX)
    6369{
    … …  
    7379
    7480ATOMIC static inline atomic_count_t atomic_postdec(atomic_t *val)
     81    WRITES(&val->count)
     82    REQUIRES_EXTENT_MUTABLE(val)
    7583    REQUIRES(val->count > ATOMIC_COUNT_MIN)
    7684{
    … …  
    8997
    9098ATOMIC static inline atomic_count_t test_and_set(atomic_t *val)
     99    WRITES(&val->count)
     100    REQUIRES_EXTENT_MUTABLE(val)
    91101{
    92102        /* On real hardware the retrieving of the original
    … …  
    99109}
    100110
    101 ATOMIC static inline atomic_count_t arch_atomic_get(atomic_t *val)
    102 {
    103         /* This function is not needed on real hardware, it just
    104            duplicates the functionality of atomic_get(). It is
    105            defined here because atomic_get() is an inline function
    106            declared in a header file which we are included in. */
    107        
    108         return val->count;
    109 }
    110 
    111111static inline void atomic_lock_arch(atomic_t *val)
     112    WRITES(&val->count)
     113    REQUIRES_EXTENT_MUTABLE(val)
    112114{
    113115        do {
    114                 while (arch_atomic_get(val));
     116                while (val->count);
    115117        } while (test_and_set(val));
    116118}

  • kernel/generic/include/atomic.h

    r09a0bd4a r33c4f72  
    4141
    4242ATOMIC static inline void atomic_set(atomic_t *val, atomic_count_t i)
     43    WRITES(&val->count)
     44    REQUIRES_EXTENT_MUTABLE(val)
    4345{
    4446        val->count = i;
    … …  
    4648
    4749ATOMIC static inline atomic_count_t atomic_get(atomic_t *val)
     50    REQUIRES_EXTENT_MUTABLE(val)
    4851{
    4952        return val->count;

  • kernel/generic/include/verify.h

    r09a0bd4a r33c4f72  
    3939#ifdef CONFIG_VERIFY_VCC
    4040
    41 #define ATOMIC         __spec_attr("atomic_inline", "")
    42 #define REQUIRES(...)  __requires(__VA_ARGS__)
     41#define ATOMIC         __specification_attr("atomic_inline", "")
     42#define READS(...)     __specification(reads(__VA_ARGS__))
     43#define WRITES(...)    __specification(writes(__VA_ARGS__))
     44#define REQUIRES(...)  __specification(requires __VA_ARGS__)
     45
     46#define REQUIRES_EXTENT_MUTABLE(...) \
     47        REQUIRES(\extent_mutable(__VA_ARGS__))
    4348
    4449#else /* CONFIG_VERIFY_VCC */
    4550
    4651#define ATOMIC
     52#define READS(...)
     53#define WRITES(...)
    4754#define REQUIRES(...)
     55
     56#define REQUIRES_EXTENT_MUTABLE(...)
    4857
    4958#endif /* CONFIG_VERIFY_VCC */

  • tools/checkers/vcc.py

    r09a0bd4a r33c4f72  
    4545re_va_list = re.compile("__builtin_va_list")
    4646
     47specification = ""
     48
    4749def usage(prname):
    4850        "Print usage syntax"
    … …  
    5759        "Preprocess source using GCC preprocessor and compatibility tweaks"
    5860       
     61        global specification
     62       
    5963        args = ['gcc', '-E']
    6064        args.extend(options.split())
    … …  
    6973       
    7074        tmpf = file(tmpfname, "w")
    71        
    72         tmpf.write("__specification(const char * const \\declspec_atomic_inline;)\n\n");
    73        
    74         tmpf.write("#define __spec_attr(key, value) \\\n");
    75         tmpf.write("    __declspec(System.Diagnostics.Contracts.CodeContract.StringVccAttr, \\\n");
    76         tmpf.write("        key, value)\n\n");
     75        tmpf.write(specification)
    7776       
    7877        for line in preproc.splitlines():
    … …  
    155154                # Run Vcc
    156155                print " -- %s --" % srcfname           
    157                 retval = subprocess.Popen([vcc_path, '/pointersize:32', cygpath(tmpfqname)]).wait()
     156                retval = subprocess.Popen([vcc_path, '/pointersize:32', '/newsyntax', cygpath(tmpfqname)]).wait()
    158157               
    159158                if (retval != 0):
    … …  
    170169
    171170def main():
     171        global specification
     172       
    172173        if (len(sys.argv) < 2):
    173174                usage(sys.argv[0])
    … …  
    192193                return
    193194       
     195        specpath = os.path.join(rootdir, "tools/checkers/vcc.h")
     196        if (not os.path.isfile(specpath)):
     197                print "%s not found." % config
     198                return
     199       
     200        specfile = file(specpath, "r")
     201        specification = specfile.read()
     202        specfile.close()
     203       
    194204        for job in jobs:
    195205                if (not vcc(vcc_path, rootdir, job)):
Note: See TracChangeset for help on using the changeset viewer.