--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on January 2020 ---
Thank you for the detailed answer. I will do manual smoke tests for now then // Nauck On Mon, Jan 13, 2020 at 12:14 PM Loïc Correnson <loic.correnson at cea.fr> wrote: > > How do I know if I get another false positive again? > > The Frama-C/WP simplifiers are checked with an extensive base of test > cases, build from community feedback and industrial test cases. > Bitwise operations have been widely exercised during the last 5 years, but > they are the more complex Frama-C simplifiers we have ever developed. > Hence, we might still find some (hopefully rare) bugs in them. > > We are working on two directions to improve this situation: > > 1. Smoke tests: this is an automated way of trying to prove (!P) instead > of P in order to detect specification inconsistencies or bugs. > 2. Formally verified simplifiers: use only simplification routines that > have been proved with Why-3 and Coq or SMT solvers. > > We hope to release (1) during 2020 ; (2) is an on-going, long-term > research work and we have an opened PhD position on this subject. > > Regards, > L. > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200116/a783e63d/attachment.html>