| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0001806 | Frama-C | Plug-in > wp | public | 2014-06-12 09:53 | 2020-02-17 18:08 | ||||
| Reporter | davyg | ||||||||
| Assigned To | correnson | ||||||||
| Priority | normal | Severity | minor | Reproducibility | have not tried | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Neon-20140301 | ||||||||
| Target Version | Fixed in Version | Frama-C 20-Calcium | |||||||
| Summary | 0001806: Error in coq code generated by wp | ||||||||
| Description | 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". | ||||||||
| Steps To Reproduce | 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) | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
correnson (manager) 2019-10-17 14:35 Last edited: 2019-10-17 14:35 |
Fixed in upcoming 20.0 (Calcium) release |
|
signoles (manager) 2020-02-17 18:08 |
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 |