2020-12-05 00:38 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001806Frama-CPlug-in > wppublic2020-02-17 18:08
Reporterdavyg 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
Product VersionFrama-C Neon-20140301 
Target VersionFixed in VersionFrama-C 20-Calcium 
Summary0001806: Error in coq code generated by wp
DescriptionThere 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".
Steps To ReproduceJust 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)
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0006885

correnson (manager)

Last edited: 2019-10-17 14:35

View 2 revisions

Fixed in upcoming 20.0 (Calcium) release

~0006946

signoles (manager)

Fixed in Frama-C 20.0 (Calcium).
+Notes

-Issue History
Date Modified Username Field Change
2014-06-12 09:53 davyg New Issue
2014-06-12 09:53 davyg Status new => assigned
2014-06-12 09:53 davyg Assigned To => correnson
2014-06-12 12:53 correnson Relationship added duplicate of 0001587
2014-06-12 12:55 correnson Relationship deleted 0001587
2019-10-17 14:35 correnson Note Added: 0006885
2019-10-17 14:35 correnson Status assigned => resolved
2019-10-17 14:35 correnson Resolution open => fixed
2019-10-17 14:35 correnson Note Edited: 0006885 View Revisions
2020-02-17 18:06 signoles Fixed in Version => Frama-C 20-Calcium
2020-02-17 18:08 signoles Status resolved => closed
2020-02-17 18:08 signoles Note Added: 0006946
+Issue History