Le 03/04/2019 à 21:51, Julia Lawall a écrit : > The why3 manual says that the smoke detector can give false positives in > the case of unreachable code. Is there any way to avoid this? I have an > unreachable match case. I tried putting absurd in the code, but I still > get a smoke detected report.
Currently there is no way. Incoherent axiomatic and unreachable code are quite similar. The only difference is from where comes the hypothesis that participates in the unsatisfiability. Your idea to use the presence of absurd is interesting. It doesn't prove that it is a false positive, but it could be used to prioritized the results of the smoke detector. Best, -- François _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
