Can't pass pipeline due to Splint warnings

training
1

What happens

Hi. I’m solving challenge 172 from Codeabbey with C. I’ve been for several days solving Splint warnings (this is my first time using C this way). Now I’m stuck with two particular kinds of warning: “Possible out-of-bounds store” and “Statement has no effect” (I’m getting it in a print function).

In addition, I’m getting a warning that says: “Unrecognized identifier: strtok_r”. I’m not sure if there is a way to use the strtok_r function, or what can I use instead.

What do you understand or find about that problem

I understand that to solve the first kind of problem, “Possible out-of-bounds store”, I need to use the annotation “requires maxSet”, but I still cannot find the right way to use it.

You make any workaround? What did you do?

I’ve been reading the Splint documentation, searching some related posts (mainly in StackOverflow), and even reading some codes in C that I found in the repo, but I still don’t get a way to solve it.

Evidences

imagen
[link to pipeline] https://gitlab.com/autonomicmind/challenges/-/commit/adb991a9e6a5cc4838cbffb1d6a1846ad54f6b8e

I need help with

I need help to understand the right way to use the annotation “requires maxSet”, or to know if there is another way to solve that kind of warning. Also, I need some advice to solve the other two warnings.

Thanks in advance!

2

You can search for answers on the repo too.

I found this one on the repo:

/*Function that clear an used string with size of MAX_SIZE*/
static void clean_string (/*@reldef@*/ char *str)
  /*@modifies str@*/ /*@requires maxSet(str) >= 0@*/ {
  int i = 0;
  for (i = 0; i < MAX_SIZE; i++) {
    str[i] = '\0';
  }
}

there you can found a way to use maxSet, but my advice is that you shouldn’t modify any param that you receive, for example right now is not allowed the use of /@modifies str@/ because we are working right now with functional programming, for that mutation aren’t allowed.

The expected comment is /*@modifies nothing@*/

On the other hand, you shouldn’t use /@/.

This file can be a little example to work with C:

https://gitlab.com/autonomicmind/challenges/blob/ea97fba35e9ec4db67287e463b91951251699cf9/code%2Fcodeabbey%2F032%2Fslayfer1112.c

Take in mind that right now that code shouldn’t pass for the use of the for the cycle and the mutation of survivors, j, z, and i.

But there you can found the main idea of the annotations.

I hope that this can help.