--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on September 2020 ---
Thanks for this report. The native Coq output of WP is deprecated and does not handle recent WP features such as IEEE floats. We are sorry about that. However, the upcoming next release of Frama-C/WP will offer full support of Coq prover via Why3, which means more predictable, more stable and full featured output. Regards, L. > Le 25 sept. 2020 à 19:19, Joshua Miller <joshmi at umich.edu> a écrit : > > I have been attempting to generate Coq code using ACSL specifications in order to manually prove anything that cannot be handled by Alt-Ergo or Z3. An issue that occurs quite often is that in the auto-generated Coq code, I get the following error: > > Goal > let x := ((L_int_pow 2%Z 4%Z))%Z in > forall (t_1 t : array Z), > forall (t_3 t_2 : farray addr Z), > forall (a : addr), > ((0 < x)%Z) -> > ((((region ((base a))%Z)) <= 0)%Z) -> > ((x <= 2147483647)%Z) -> > ((linked t)) -> > ((sconst t_2)) -> > ((P_valid_read_string t_1 t_3 ((shift_sint8 ((global (Str_39)%Z)) 0%Z)))) -> > ((P_valid_read_string t_1 t_3 ((shift_sint8 ((global (Str_40)%Z)) 0%Z)))) -> > ((is_finite_f64 ( 1 / 5 )%R%R)). > > Where the bold red "1 / 5" throws the issue of being type "real" while it is expected to have type "f64". This is a simple enough issue to fix by manually casting "to_f64(1 / 5)" and then solving in Coq, but this code is auto-generated each time. This means anything I put within the actual proof will remain, but my typecast will not. I have not been able to determine a way to trace this code to anywhere in the original C code, otherwise I would try changing the source. Any suggestions are welcome. > > Best, > > Joshua Miller > _______________________________________________ > 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/20200928/0ee966d5/attachment.html>