Fork us on GitHub Follow us on Facebook Follow us on Twitter

Changeset 09a0bd4a in mainline


Ignore:
Timestamp:
2010-06-24T13:00:16Z (11 years ago)
Author:
Martin Decky <martin@…>
Branches:
master
Children:
2d03471, 33c4f72
Parents:
e821e49
Message:

initial properties annotation and verification support
(does not do much yet, but also does not stand in the way)

Files:
1 added
4 edited

Legend:

Unmodified
Added
Removed
  • kernel/arch/abs32le/include/atomic.h

    re821e49 r09a0bd4a  
    3939#include <arch/barrier.h>
    4040#include <preemption.h>
     41#include <verify.h>
    4142
    42 static inline void atomic_inc(atomic_t *val) {
     43ATOMIC static inline void atomic_inc(atomic_t *val)
     44    REQUIRES(val->count < ATOMIC_COUNT_MAX)
     45{
    4346        /* On real hardware the increment has to be done
    4447           as an atomic action. */
     
    4750}
    4851
    49 static inline void atomic_dec(atomic_t *val) {
     52ATOMIC static inline void atomic_dec(atomic_t *val)
     53    REQUIRES(val->count > ATOMIC_COUNT_MIN)
     54{
    5055        /* On real hardware the decrement has to be done
    5156           as an atomic action. */
    5257       
    53         val->count++;
     58        val->count--;
    5459}
    5560
    56 static inline atomic_count_t atomic_postinc(atomic_t *val)
     61ATOMIC static inline atomic_count_t atomic_postinc(atomic_t *val)
     62    REQUIRES(val->count < ATOMIC_COUNT_MAX)
    5763{
    5864        /* On real hardware both the storing of the previous
     
    6672}
    6773
    68 static inline atomic_count_t atomic_postdec(atomic_t *val)
     74ATOMIC static inline atomic_count_t atomic_postdec(atomic_t *val)
     75    REQUIRES(val->count > ATOMIC_COUNT_MIN)
    6976{
    7077        /* On real hardware both the storing of the previous
     
    8188#define atomic_predec(val)  (atomic_postdec(val) - 1)
    8289
    83 static inline atomic_count_t test_and_set(atomic_t *val)
     90ATOMIC static inline atomic_count_t test_and_set(atomic_t *val)
    8491{
     92        /* On real hardware the retrieving of the original
     93           value and storing 1 have to be done as a single
     94           atomic action. */
     95       
    8596        atomic_count_t prev = val->count;
    8697        val->count = 1;
     
    8899}
    89100
     101ATOMIC 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
    90111static inline void atomic_lock_arch(atomic_t *val)
    91112{
    92113        do {
    93                 while (val->count);
     114                while (arch_atomic_get(val));
    94115        } while (test_and_set(val));
    95116}
  • kernel/arch/abs32le/include/types.h

    re821e49 r09a0bd4a  
    3535#ifndef KERN_abs32le_TYPES_H_
    3636#define KERN_abs32le_TYPES_H_
     37
     38#define ATOMIC_COUNT_MIN  UINT32_MIN
     39#define ATOMIC_COUNT_MAX  UINT32_MAX
    3740
    3841typedef uint32_t size_t;
  • kernel/generic/include/atomic.h

    re821e49 r09a0bd4a  
    3838#include <typedefs.h>
    3939#include <arch/atomic.h>
     40#include <verify.h>
    4041
    41 static inline void atomic_set(atomic_t *val, atomic_count_t i)
     42ATOMIC static inline void atomic_set(atomic_t *val, atomic_count_t i)
    4243{
    4344        val->count = i;
    4445}
    4546
    46 static inline atomic_count_t atomic_get(atomic_t *val)
     47ATOMIC static inline atomic_count_t atomic_get(atomic_t *val)
    4748{
    4849        return val->count;
  • tools/checkers/vcc.py

    re821e49 r09a0bd4a  
    5959        args = ['gcc', '-E']
    6060        args.extend(options.split())
    61         args.append(srcfname)
     61        args.extend(['-DCONFIG_VERIFY_VCC=1', srcfname])
    6262       
    6363        # Change working directory
     
    6969       
    7070        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");
    7177       
    7278        for line in preproc.splitlines():
     
    149155                # Run Vcc
    150156                print " -- %s --" % srcfname           
    151                 retval = subprocess.Popen([vcc_path, cygpath(tmpfqname)]).wait()
     157                retval = subprocess.Popen([vcc_path, '/pointersize:32', cygpath(tmpfqname)]).wait()
    152158               
    153159                if (retval != 0):
Note: See TracChangeset for help on using the changeset viewer.