Agreed, it was just the fastet example I could come up with, not even
claiming it might have any usability - considerable you might use enums
sometimes, to help the compiler, to check that only certain values for a
variable are 'valid'. formal verification is a completely different topic.
I thought of it as a rather simplistic example where leaving a variable
in certain cases unitialized is not really an error in the program's
logic and thus have a compiler produce an error might be
unwanted/unexpected behavior.
Regards
-Sven
Tom St Denis schrieb:
Sven Eschenberg wrote:
Bailing out with an error could be perfectly unreasonable.
Ideally you should use -Werror and/or perform parameter checking. a 2
mod 3 number of parameters may be "invalid" but if you don't actually
act on it your program cannot be verified.
Granted I never use -Werror as I don't care about a lot of the minor
violations (.e.g. passing a long to %d in a homebrew behind the scenes
test program).
Tom