Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001806Frama-CPlug-in > wppublic2014-06-12 09:532019-03-08 15:32
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityhave not tried
PlatformOSOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in Version 
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

-  Notes
There are no notes attached to this issue.

- 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

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker