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

  • Subject: [Frama-c-discuss] Coq Auto-generated Code Incorrect
  • From: joshmi at umich.edu (Joshua Miller)
  • Date: Fri, 25 Sep 2020 13:19:48 -0400
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200925/54ac8e33/attachment.html>