On 10/04/2014, at 4:34 AM, Shelley Dong wrote:
> Hello there,
>
> 1) I used roundf, fasbf, MAXFLOAT for my floating-point variables but
> Splint complains ‘Identifier used in code has not been declared’.
roundf() and fabsf() are from C99.
Splint is still basically a C89 checker;
has its library support been upgraded for C99?
Hmm, search search.
<splint-home>/lib/standard.lcd
is what splint actually reads,
apparently generated from
<split-home>/lib/standard.h
which mentions fabsf() but inside
#ifdef OPTIONAL_MATH
...
#endif
with a preceding comment "These functions
are optional in ISO C."
You might need to
- add round{f,,l} to this file,
- regenerate the .lcd file (with -DOPTIONAL_MATH)
I can't find any mention of MAXFLOAT in C89, C99, or C11.
The standard name is FLT_MAX (maximum representable
finite floating-point number) and it comes from <float.h>.
I suggest you replace MAXFLOAT with FLT_MAX.
> 3) I also got a suppressed warning about ‘formalarray’ which I never
> came across before and need to justify in my static analysis report.
> I am using splint 3.1.1. I looked through the Manual.pdf and found some
> descriptions. But I am still confused what may be the cause for the warning.
> Did anyone have similar warning before?
> What may be the cause? Why Splint triggers a warning for this?
> P:- formal-array (copied from Manual.pdf)
> A formal parameter is declared as an array. This is probably not a problem,
> but can be
> confusing since it is treated as a pointer.
It would help if you exhibited the code that Splint is complaining
about, but it probably looks something like
void foobar(int x[40]) { ... }
This is a "formal parameter that is declared as an array".
The thing that is confusing about it is that the 40 has
absolutely no effect; this is entirely equivalent to
void foobar(int *x) { ... }
In particular, you can pass it an that that is smaller, even much
smaller, and the C compiler won't blink. I have often seen
people writing code like this expecting the compiler to complain
if the actual parameter is not an array of the right size.
Modern C has a *different* (and weird) construction for that:
void foobar(int x[static 40]) { ... }
where now the 40 *is* part of the parameter's type and *will*
be checked.
One thing that can definitely go badly wrong is if you have
void foobar(int x[40]) {
...
use sizeof x
...
}
The answer will be sizeof (int*), not 40 * sizeof (int).
Once again, int x[static 40] is the answer.
_______________________________________________
splint-discuss mailing list
splint-discuss@mail.cs.virginia.edu
http://www.cs.virginia.edu/mailman/listinfo/splint-discuss
