[splint-discuss] Passed storage not completely defined

[Michael Wojcik]

But Perm has been initialized - it points to the same object as "array"
in main, which was initialized from the values in argv.

 

And while Permute does not operate on the contents pointed to by the
values in the Perm array, it does use those values (as it rearranges
them). So an @out@ annotation would be incorrect, even if it suppresses
the error.

 

I don't see any reasonable interpretation here other than that the
diagnostic from Splint is incorrect. In the call to Permute in main,
"*array" is identical to "array[0]", and array[0] has been initialized
unless one of the following holds:

 

- argc < 2 (and the program should have checked for this, since it
causes undefined behavior if argc==0 and implementation-defined behavior
if argc==1, both of which are possible)

- argv[1] is undefined (which should not happen in a hosted
implementation if argc >= 2, and Splint should know that)

 

Some other criticisms might be leveled against the code (why is temp in
Permute an array, when only the first element is ever used?), but unless
I'm missing something, this is an incorrect diagnostic from Splint.

 

Michael Wojcik 
Principal Software Systems Developer, Micro Focus 

 

 

 

From: splint-discuss-bounces at cs.virginia.edu
[mailto:splint-discuss-bounces at cs.virginia.edu] On Behalf Of Frayda,
Christine
Sent: Wednesday, 27 January, 2010 09:56
To: Discussions about the Splint annotation-assisted static
analysisproject
Subject: Re: [splint-discuss] Passed storage not completely defined

 

Hi Jason,

Do you consider Perm to be a "returned storage which need not be
defined," in other words, an output, not an input variable where the
function cares about the values?  If so, you can instrument the function
to check the code appropriately.

 

static void Permute(/*@out@*/ char *Perm[], size_t sizePerm, size_t
unchanged) {

 

There are many fine examples of other instrumentations in the Splint
manual.  In particular, I see an example of /*@out@*/ in chapter 3.

                Chris

 

From: splint-discuss-bounces at cs.virginia.edu
[mailto:splint-discuss-bounces at cs.virginia.edu] On Behalf Of Jason blank
Sent: Tuesday, January 26, 2010 10:07 PM
To: splint-discuss at mail.cs.virginia.edu
Subject: [splint-discuss] Passed storage not completely defined

 

Hello,

I have the following block code which works but splint throws a message:
Splint 3.1.2 --- 26 Jan 2010

Spec file not found: a.lcl
a.c: (in function main)
a.c:47:11: Passed storage array not completely defined (*array is
undefined):
              Permute (array, ...)
  Storage derivable from a parameter, return value or global is not
defined.
  Use /*@out@*/ to denote passed or returned storage which need not be
defined.
  (Use -compdef to inhibit warning)
   a.c:39:3: Storage *array allocated

Finished checking --- 1 code warning

Here is the code.  Please keep in mind I did not write Permute.  I found
it on the web.  I am trying to allocate an array where I don't know how
many elements I am going to need.  I also don't know the size of the
elements.  What did I do wrong?

#include <stdio.h>
#include <stdlib.h>

static void Permute(char *Perm[], size_t sizePerm, size_t unchanged) {
size_t outer = 0;
size_t inner = 0;
size_t t = 0;
char *temp[sizePerm];

  if(sizePerm > unchanged) {
    for(outer = unchanged; outer < sizePerm; outer++) {
      *temp = Perm[outer];
      for(inner = outer; inner > unchanged; inner--) {
        Perm[inner] = Perm[inner - 1];
      }
      Perm[unchanged] = *temp;
      Permute(Perm, sizePerm, unchanged+1);

      for(inner = unchanged; inner < outer; inner++) {
        Perm[inner] = Perm[inner + 1];
      }
      Perm[outer] = *temp;
    }
  }
  else {
    for (t=0;t<sizePerm;t++) {
      printf("%s", Perm[t]);
    }
    printf("\n");
  }
}

int main(int argc, char *argv[]) {
char **array; /* array to store words */
size_t numtodo;
size_t temp;

  numtodo=(size_t)(argc)-1;
  array=malloc(numtodo * sizeof(*array)); /*allocate size of array*/
  if (array == NULL) {
    printf("can't allocate memory for array\n");
    exit(EXIT_FAILURE);
  }
  for (temp=0; temp < numtodo; temp++) {
    array[temp] = argv[temp+1]; /*assign values to array */
  }
  Permute(array,numtodo,0);

free(array);
return 0;
}

________________________________

Hotmail: Free, trusted and rich email service. Get it now.
<http://clk.atdmt.com/GBL/go/196390708/direct/01/> 

 

Click here
<https://www.mailcontroller.altohiway.com/sr/+k4KaQkz48DTndxI!oX7UrDv!jL
6nhygOgWIAaAvUCFbgHWxFKiBr36HhRgAzFL99r4ZDktgx4dcNZBvQFKuzA==>  to
report this email as spam.

This message has been scanned for viruses by MailController
<http://www.MailController.altohiway.com/> .

No virus found in this incoming message.
Checked by AVG - www.avg.com
Version: 9.0.730 / Virus Database: 271.1.1/2638 - Release Date: 01/25/10
14:36:00

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.cs.virginia.edu/pipermail/splint-discuss/attachments/20100127/0b65e421/attachment-0001.html