Frama-C Bug Tracking System - Frama-C
View Issue Details
0001806Frama-CPlug-in > wppublic2014-06-12 09:532019-03-08 15:32
davyg 
correnson 
normalminorhave not tried
assignedopen 
Frama-C Neon-20140301 
 
0001806: Error in coq code generated by wp
There is a typing error with some code generated by wp.

For example this script :

_Bool g()
{
    return 0;
}

//@ensures x == (!!\result == !!x);
_Bool f(_Bool x)
{
    return g();
}

When using prover coq from wp generates :

Goal
  forall (f_0 x_0 : Z),
  ((is_uint32 f_0%Z)) ->
  ((is_uint32 x_0%Z)) ->
  ((((Zneq_bool 0 x_0))
    = ((Zeq_bool ((Zneq_bool 0 f_0)) ((Zneq_bool 0 x_0)))))%Z)%Z.

Proof.
(* auto with zarith. *)
Qed.

which produce this coq error on "Zneq_bool 0 f_0":

Error: In environment
f_0 : int
x_0 : int
The term "Zneq_bool 0 f_0" has type "bool" while it is expected to have type
 "int".
Just use the C example with wp/coq as prover (with the gui for example because else wp consider that the script fails and does not print the error)
No tags attached.
Issue History
2014-06-12 09:53davygNew Issue
2014-06-12 09:53davygStatusnew => assigned
2014-06-12 09:53davygAssigned To => correnson
2014-06-12 12:53corrensonRelationship addedduplicate of 0001587
2014-06-12 12:55corrensonRelationship deleted0001587

There are no notes attached to this issue.