]> andersk Git - splint.git/blame - test/globalbufferannotation/globalvariable.c
*** empty log message ***
[splint.git] / test / globalbufferannotation / globalvariable.c
CommitLineData
ed3a6c22 1//#include "/home/drl7x/re/LCLintDev/lib/ansi.h"
2
3static char f [12];
4extern void /*@alt char * @*/
5 mstrcpy (/*@unique@*/ /*@out@*/ /*returned*/ char *s1, char *s2)
d9a28762 6 /*@modifies *s1@*/ /*@requires MaxSet(s1) >= MaxRead(s2); @*/;
ed3a6c22 7
8
d9a28762 9void copyf (char * c) /*@requires MaxSet(c) >= MaxRead(f); @*/
ed3a6c22 10{
11 mstrcpy (c, f);
12}
This page took 0.053314 seconds and 5 git commands to generate.