Changeset 33c4f72 in mainline for kernel


Ignore:
Timestamp:
2010-06-25T13:38:30Z (15 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

Location:
kernel
Files:
3 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 */
Note: See TracChangeset for help on using the changeset viewer.