-
Notifications
You must be signed in to change notification settings - Fork 76
Open
Description
Hello, the following is a simple program that, when passed to splint, makes it loop forever without returning a value.
void foo(int *, int* k) {
*k++;
}
When saved as foo.c, splint foo.c will not finish.
A backtrace when running splint under gdb:
#0 usymtab_lookupSafeScope (k=0x0, lexlevel=lexlevel@entry=0) at usymtab.c:5058
#1 0x0000555555606394 in sRef_updateSref (s=0x55555580a2e0) at sRef.c:956
#2 0x00005555556065ad in sRef_aliasCheckSimplePred (predf=predf@entry=0x5555556046e0 <sRef_isExternallyVisibleAux>, s=s@entry=0x55555580a4b0) at sRef.c:8382
#3 0x000055555560666f in sRef_isExternallyVisible (s=s@entry=0x55555580a4b0) at sRef.c:879
#4 0x000055555564e27e in constraintList_makeFixedArrayConstraints (s=0x55555580c2a0) at constraintGeneration.c:479
#5 0x000055555564e2e9 in exprNode_generateConstraints (e=0x55555580c210) at constraintGeneration.c:144
#6 exprNode_generateConstraints (e=e@entry=0x55555580c210) at constraintGeneration.c:109
#7 0x0000555555644bc4 in exprNode_checkFunction (ue=0x55555580a040, body=body@entry=0x55555580c210) at exprChecks.c:972
#8 0x00005555555700c4 in yyparse () at cgrammar.c:4338
Metadata
Metadata
Assignees
Labels
No labels