test/manual/exposure.c

   1 # include "employee.h"
   2
   3 char *
   4 employee_getName (employee e)
   5 {
   6   return e->name;
   7 }
   8
   9 /*@observer@*/ char *
  10 employee_obsName (employee e)
  11 { return e->name; }
  12
  13 /*@exposed@*/ char *
  14 employee_exposeName (employee e)
  15 { return e->name; }
  16
  17 void
  18 employee_capName (employee e)
  19 {
  20   char *name;
  21
  22   name = employee_obsName (e);
  23   *name = toupper (*name);
  24 }
  25
  26