2 ensures.c: (in function notnullname)
3 ensures.c:6:4: Dereference of possibly null pointer *name: **name
4 ensures.c:7:2: Possibly null storage *name corresponds to storage listed in
6 ensures.c: (in function nullname)
7 ensures.c:13:2: Non-null storage *name corresponds to storage listed in ensures
9 ensures.c: (in function callname)
10 ensures.c:33:4: Dereference of null pointer *s: **s
11 ensures.c:32:3: Storage *s becomes null
13 Finished checking --- 4 code warnings, as expected