]>
Commit | Line | Data |
---|---|---|
77970e15 | 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 |