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

PS: the alternative to benefit from Coq inside Frama-C/WP is use a dedicated WP driver to import extern Why3 theories in the proof context (See WP manual section 2.3.11).
You can then state your lemmas in a Why3 theory, and prove them in Coq by using Why3 IDE, and finally WP can use them when calling SMT solvers.


> 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/6a25dcfe/attachment.html>