[splint-discuss] Exporting declarations

[splint at coreland.ath.cx]

On 2009-05-26 06:53:33, Jonathan and Caroline Moore wrote:
> Are you returning something with static duration?
> 
> Some code fragments will help pin down the insecurity splint is highlighting.
> 

Uh, the entire file is:

#ifndef COPY_H
#define COPY_H

void copy (char [], char []);

#endif

I don't think the problem is related to storage. I think splint is saying
I need to place the function in a specification.

Sort of answered my own question...

$ cat copy.lcl
void
copy (char source[], char target[])
{
  requires nullTerminated (source^);
  modifies target;
  ensures lenStr (target') >= lenStr (source^);
}

Splint seems happy with the above.