Splint warnings about dependent storage returned as implicitly only.

[luser- -droog]

I'm trying get my code to pass splint and I'm having difficulty understanding the warnings. I've read up on Splint's memory model (http://www.splint.org/manual/html/sec5.html), but my use of memory is very, very different.

I'm doing sub-allocation within big malloc'ed regions, with a custom garbage-collector. So I want just the minimum annotations to keep splint happy.

Here are the errors I'm looking at:

$ make splint
splint +posixlib -boolops -predboolint +ignoresigns -type -nestcomment \
-shiftimplementation -predboolothers -exportlocal -mustfreefresh ./*.c
Splint 3.1.2 --- 15 Sep 2012

di.c: (in function diclookup)
di.c:195:85: Dependent storage tp returned as implicitly only: tp + (2 * i)
Dependent storage is transferred to a non-dependent reference. (Use
-dependenttrans to inhibit warning)
di.c:188:48: Storage tp becomes dependent
di.c:195:96: Released storage mem->base reachable from parameter at return
point
Memory is used after it has been released (either by passing as an only param
or assigning to an only global). (Use -usereleased to inhibit warning)
di.c:195:85: Storage mem->base released
di.c:197:86: Dependent storage tp returned as implicitly only: tp + (2 * i)
di.c:188:48: Storage tp becomes dependent
di.c:197:97: Released storage mem->base reachable from parameter at return
point
di.c:197:86: Storage mem->base released
di.c:200:86: Dependent storage tp returned as implicitly only: tp + (2 * i)
di.c:188:48: Storage tp becomes dependent
di.c:200:97: Released storage mem->base reachable from parameter at return
point
di.c:200:86: Storage mem->base released
di.c: (in function dicget)
di.c:218:11: Index of possibly null pointer e: e
A possibly null pointer is dereferenced. Value is either the result of a
function which may return null (in which case, code should check it is not
null), or a global, parameter or structure field declared with the null
qualifier. (Use -nullderef to inhibit warning)
di.c:217:6: Storage e may become null


All of this is in my dictionary (hash-table) lookup functions

177
178 #define RETURN_TAB_I_IF_EQ_K_OR_NULL \
179 if (objcmp(ctx, tp[2*i], k) == 0 \
180 || objcmp(ctx, tp[2*i], null) == 0) \
181 return tp + (2*i);
182
183 /* perform a hash-assisted lookup.
184 returns a pointer to the desired pair (if found)), or a null-pair. */
185 /*@null@*/ object *diclookup(context *ctx, mfile *mem, object d, object k) {
186 unsigned ad = adrent(mem, d.comp_.ent);
187 dichead *dp = (void *)(mem->base + ad);
188 object *tp = (void *)(mem->base + ad + sizeof(dichead));
189 unsigned sz = (dp->sz + 1);
190 unsigned h;
191 unsigned i;
192 h = hash(k) % sz;
193 i = h;
194
195 RETURN_TAB_I_IF_EQ_K_OR_NULL
196 for (++i; i < sz; i++) {
197 RETURN_TAB_I_IF_EQ_K_OR_NULL
198 }
199 for (i=0; i < h; i++) {
200 RETURN_TAB_I_IF_EQ_K_OR_NULL
201 }
202 return NULL; /* i == h : dict is overfull: no null entry */
203 }
204
205 /* see if lookup returns a non-null pair. */
206 bool dicknown(context *ctx, mfile *mem, object d, object k) {
207 object *r;
208 r = diclookup(ctx, mem, d, k);
209 if (r == NULL) return false;
210 return type(*r) != nulltype;
211 }
212
213 /* call diclookup,
214 return the value if the key is non-null. */
215 object dicget(context *ctx, mfile *mem, object d, object k) {
216 object *e;
217 e = diclookup(ctx, mem, d, k);
218 if (type(e[0]) == nulltype)
219 error("undefined");
220 return e[1];
221 }

Full file: http://code.google.com/p/xpost/source/browse/di.c

The NULL stuff I probably need to triple-check again, so I don't want to silence that one. For the others, does it make sense to just mark everything /*@dependent@*/ ?


--
true oog

[luser- -droog]

On Monday, May 20, 2013 1:00:23 AM UTC-5, luser- -droog wrote:
> I'm trying get my code to pass splint and I'm having difficulty understanding the warnings. I've read up on Splint's memory model (http://www.splint.org/manual/html/sec5.html), but my use of memory is very, very different.
>
>
>
> I'm doing sub-allocation within big malloc'ed regions, with a custom garbage-collector. So I want just the minimum annotations to keep splint happy.
>
>
>
> Here are the errors I'm looking at:
>
>
>
> $ make splint
>
> splint +posixlib -boolops -predboolint +ignoresigns -type -nestcomment \
>
> -shiftimplementation -predboolothers -exportlocal -mustfreefresh ./*.c
>
> Splint 3.1.2 --- 15 Sep 2012
>
>
>
> di.c: (in function diclookup)
>
> di.c:195:85: Dependent storage tp returned as implicitly only: tp + (2 * i)
>
> Dependent storage is transferred to a non-dependent reference. (Use
>
> -dependenttrans to inhibit warning)
>

[snip]

> Full file: http://code.google.com/p/xpost/source/browse/di.c
>
>
>
> The NULL stuff I probably need to triple-check again, so I don't want to silence that one. For the others, does it make sense to just mark everything /*@dependent@*/ ?
>

That seems to do it. I annotated all the mfiles, the structure that holds the malloc'ed data bank, with /*@dependent@*/ and splint lets it fly.

So, I suppose I'm not hurting for answers or anything. Thanks for your time.

However, if anybody has any relevant knowledge on what /*@dependent@*/ is really supposed to be for, and whether my fix is any better (eek!) than just inhibiting the warnings with the command option, I'd be happy to learn it.