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