splint -strict example1.c
Splint 3.1.2 --- 11 May 2019
example1.c: (in function main)
example1.c:9:5: Format string parameter to printf is not a compile-time
                   constant: buffer
  Format parameter is not known at compile-time.  This can lead to security
  vulnerabilities because the arguments cannot be type checked. (Use
  -formatconst to inhibit warning)
example1.c:9:5: 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)
example1.c:9:5: Undocumented modification of file system state possible from
                   call to printf: printf(buffer)
  report undocumented file system modifications (applies to unspecified
  functions if modnomods is set) (Use -modfilesys to inhibit warning)
example1.c:10:4: Path with no return in function declared to return int
  There is a path through a function declared to return a value on which there
  is no return statement. This means the execution may fall through without
  returning a meaningful result to the caller. (Use -noret to inhibit warning)
example1.c:8:5: Possible out-of-bounds store: strcpy(buffer, argv[1])
    Unable to resolve constraint:
    requires maxRead(argv[1] @ example1.c:8:20) <= 9
     needed to satisfy precondition:
    requires maxSet(buffer @ example1.c:8:12) >= maxRead(argv[1] @
    example1.c:8:20)
     derived from strcpy precondition: requires maxSet(<parameter 1>) >=
    maxRead(<parameter 2>)
  A memory write may write to an address beyond the allocated buffer. (Use
  -boundswrite to inhibit warning)
example1.c:8:20: Possible out-of-bounds read: argv[1]
    Unable to resolve constraint:
    requires maxRead(argv @ example1.c:8:20) >= 1
     needed to satisfy precondition:
    requires maxRead(argv @ example1.c:8:20) >= 1
  A memory read references memory beyond the allocated storage. (Use
  -boundsread to inhibit warning)
example1.c:5: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 --- 7 code warnings