--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on January 2011 ---
Hello Pascal, 2011/1/11 Pascal Cuoq <pascal.cuoq at gmail.com>: > The difference is that (unless perhaps for very special compilation > platforms) the programmer probably did not divide by zero on purpose, > since that halts the program. Divisions by zero, if they > really happen, are the border cases that were not encountered during > testing (they would have been fixed if they had). The dependency flow > is probably correct despite the borderline cases. More importantly, > tool and human agree on what an incorrect execution is (an execution > that is abruptly terminated by a hardware exception is an > incorrect execution). > > A "benign alarm", on the other hand, may be an inconsequential > idiom in the code. Tests did not reveal anything was wrong (indeed, > the code was working as the programmer intended). It can happen > in a large proportion of executions, and therefore hide most of the > behavior of the program from the analysis. The tool calls "incorrect" > some executions that look perfectly normal to the human, and > that the human would have liked to see included in the synthetic > results. That's clearer, thanks. Regards, d.