--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on January 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Strange results when verifying bitshifts using frama-c v19.1 with z3



> 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.