See www.splint.org for information on the splint program.


% splint h0.c
Splint 3.1.1 --- 15 Jun 2004

h0.c: (in function main)
h0.c:20:14: Parameter argc not used
  A function parameter is not used in the body of the function. If the argument
  is needed for type compatibility or future plans, use /*@unused@*/ in the
  argument declaration. (Use -paramuse to inhibit warning)

Finished checking --- 1 code warning


% splint h1.c
Splint 3.1.1 --- 15 Jun 2004

Finished checking --- no warnings


% splint -strict-lib h0.c
Splint 3.1.1 --- 15 Jun 2004

h0.c: (in function f1)
h0.c:12:3: Return value (type int) ignored: printf("%4d  f1\...
  Result returned by function call is not used. If this is intended, can cast
  result to (void) to eliminate message. (Use -retvalint to inhibit warning)
h0.c: (in function f2)
h0.c:17:3: Return value (type int) ignored: printf("%4d  f2 ...
h0.c: (in function main)
h0.c:29:3: Return value (type int) ignored: printf("main out\n")
h0.c:20:14: Parameter argc not used
  A function parameter is not used in the body of the function. If the argument
  is needed for type compatibility or future plans, use /*@unused@*/ in the
  argument declaration. (Use -paramuse to inhibit warning)

Finished checking --- 4 code warnings


% splint -strict-lib h1.c
Splint 3.1.1 --- 15 Jun 2004

h1.c: (in function f1)
h1.c:14:3: Called procedure printf may access global stdout
  A checked global variable is used in the function, but not listed in its
  globals clause. By default, only globals specified in .lcl files are checked.
  To check all globals, use +allglobals. To check globals selectively use
  /*@checked@*/ in the global declaration. (Use -globs to inhibit warning)
h1.c:14:3: Undocumented modification of *stdout possible from call to printf:
              printf("%4d  f1\n", n)
  An externally-visible object is modified by a function, but not listed in its
  modifies clause. (Use -mods to inhibit warning)
h1.c:14:3: Return value (type int) ignored: printf("%4d  f1\...
  Result returned by function call is not used. If this is intended, can cast
  result to (void) to eliminate message. (Use -retvalint to inhibit warning)
h1.c: (in function f2)
h1.c:19:3: Called procedure printf may access global stdout
h1.c:19:3: Undocumented modification of *stdout possible from call to printf:
              printf("%4d  f2 ***\n", n)
h1.c:19:3: Return value (type int) ignored: printf("%4d  f2 ...
h1.c: (in function main)
h1.c:31:3: Called procedure printf may access global stdout
h1.c:31:3: Undocumented modification of *stdout possible from call to printf:
              printf("main out\n")
h1.c:31:3: Return value (type int) ignored: printf("main out\n")

Finished checking --- 9 code warnings


% splint -posix-strict-lib h0.c
Splint 3.1.1 --- 15 Jun 2004

h0.c: (in function f1)
h0.c:12:3: Return value (type int) ignored: printf("%4d  f1\...
  Result returned by function call is not used. If this is intended, can cast
  result to (void) to eliminate message. (Use -retvalint to inhibit warning)
h0.c: (in function f2)
h0.c:17:3: Return value (type int) ignored: printf("%4d  f2 ...
h0.c: (in function main)
h0.c:29:3: Return value (type int) ignored: printf("main out\n")
h0.c:20:14: Parameter argc not used
  A function parameter is not used in the body of the function. If the argument
  is needed for type compatibility or future plans, use /*@unused@*/ in the
  argument declaration. (Use -paramuse to inhibit warning)

Finished checking --- 4 code warnings


% splint -posix-strict-lib h1.c
Splint 3.1.1 --- 15 Jun 2004

h1.c: (in function f1)
h1.c:14:3: Called procedure printf may access global stdout
  A checked global variable is used in the function, but not listed in its
  globals clause. By default, only globals specified in .lcl files are checked.
  To check all globals, use +allglobals. To check globals selectively use
  /*@checked@*/ in the global declaration. (Use -globs to inhibit warning)
h1.c:14:3: Undocumented modification of *stdout possible from call to printf:
              printf("%4d  f1\n", n)
  An externally-visible object is modified by a function, but not listed in its
  modifies clause. (Use -mods to inhibit warning)
h1.c:14:3: Return value (type int) ignored: printf("%4d  f1\...
  Result returned by function call is not used. If this is intended, can cast
  result to (void) to eliminate message. (Use -retvalint to inhibit warning)
h1.c: (in function f2)
h1.c:19:3: Called procedure printf may access global stdout
h1.c:19:3: Undocumented modification of *stdout possible from call to printf:
              printf("%4d  f2 ***\n", n)
h1.c:19:3: Return value (type int) ignored: printf("%4d  f2 ...
h1.c: (in function main)
h1.c:31:3: Called procedure printf may access global stdout
h1.c:31:3: Undocumented modification of *stdout possible from call to printf:
              printf("main out\n")
h1.c:31:3: Return value (type int) ignored: printf("main out\n")

Finished checking --- 9 code warnings

----------------------------------------------------------------------------------

% .../splint-3.1.2/bin/splint +strict +unixlib h1.c
Splint 3.1.2 --- 19 Mar 2012

h1.c: (in function main)
h1.c:29:3: Statement has no effect (possible undected modification through call
              to unconstrained function ): (*func)()
  Statement has no visible effect --- no values are modified. It may modify
  something through a call to an unconstrained function. (Use -noeffectuncon to
  inhibit warning)
h1.c:31:3: Called procedure printf may access file system state, but globals
              list does not include globals fileSystem
  A called function uses internal state, but the globals list for the function
  being checked does not include internalState (Use -internalglobs to inhibit
  warning)
h1.c:31:3: Undocumented modification of file system state possible from call to
              printf: printf("main out\n")
  report undocumented file system modifications (applies to unspecified
  functions if modnomods is set) (Use -modfilesys to inhibit warning)
h1.c:27:3: Possible out-of-bounds store: A[n = atoi(argv[1])]
    Unable to resolve constraint:
    requires n = atoi(argv[1]) @ h1.c:27:5 <= 1
     needed to satisfy precondition:
    requires maxSet(A @ h1.c:27:3) >= n = atoi(argv[1]) @ h1.c:27:5
  A memory write may write to an address beyond the allocated buffer. (Use
  -boundswrite to inhibit warning)
h1.c:27:14: Possible out-of-bounds read: argv[1]
    Unable to resolve constraint:
    requires maxRead(argv @ h1.c:27:14) >= 1
     needed to satisfy precondition:
    requires maxRead(argv @ h1.c:27:14) >= 1
  A memory read references memory beyond the allocated storage. (Use
  -boundsread to inhibit warning)
h1.c:29:4: Possible out-of-bounds read: *func
    Unable to resolve constraint:
    requires maxRead(f1 @ h1.c:24:24) >= 0
     needed to satisfy precondition:
    requires maxRead(func @ h1.c:29:5) >= 0

Finished checking --- 6 code warnings

----------------------------------------------------------------------------------
%