Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Coq Auto-generated Code Incorrect

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>