Frama-C Bug Tracking System - Frama-C | ||||||||||
View Issue Details | ||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | |||||
0002401 | Frama-C | Plug-in > wp | public | 2018-10-01 10:01 | 2019-10-17 18:00 | |||||
Reporter | jmaytac | |||||||||
---|---|---|---|---|---|---|---|---|---|---|
Assigned To | correnson | |||||||||
Priority | normal | Severity | major | Reproducibility | always | |||||
Status | closed | Resolution | no change required | |||||||
Platform | OS | OS Version | ||||||||
Product Version | Frama-C 17-Chlorine | |||||||||
Target Version | Fixed in Version | |||||||||
Summary | 0002401: Newer releases of FramaC produce apparent WP plug-in bug | |||||||||
Description | The code in the attached example models a reactive program which interacts with peripherals via memory mapped I/O through an address defined by a constant. While an older version of frama-C (Phosphorus) successfully produced Altergo axiomatizations of boolean logic functions like the "logic boolean isAMessage(mac_t mac)" defined in mac.h, " logic boolean isAMessage(mac_t mac) = ((mac->mac_packet.object_high == 0x0A) && (mac->mac_packet.object_low == 0x0A) && (mac->\ mac_packet.payload_length == 0x00)); " the newer versions produce as AltErgo axiomatization (see out/typed/Axiomatic11.ergo in the attached) " function L_isAMessage () : bool = andb(eqb(#{w_0}, 0), andb(eqb(#{w_1}, 10), eqb(#{w_2}, 10))) " Note that the argument to the boolean logic function is absent and the mac_t fields referenced in the ACSL definition of the logic function have. become "#{w_i}" - this malformed AltErgo (# is illegal in AltErgo) seems to originates from WP's QED module's pretty printer, whose find_var_env function returns these malformed names when it fails to find a given name in its environment. | |||||||||
Steps To Reproduce | tar -xvf framaBug.tar.gz make wp | |||||||||
Tags | No tags attached. | |||||||||
Relationships |
| |||||||||
Attached Files | ![]() https://bts.frama-c.com/file_download.php?file_id=1284&type=bug ![]() https://bts.frama-c.com/file_download.php?file_id=1286&type=bug |
Notes | |||||
|
|||||
|
|
||||
|
|||||
|
|
||||
|
|||||
|
|
||||
|
|||||
|
|
Issue History | |||||
Date Modified | Username | Field | Change | ||
---|---|---|---|---|---|
2018-10-01 10:01 | jmaytac | New Issue | |||
2018-10-01 10:01 | jmaytac | Status | new => assigned | ||
2018-10-01 10:01 | jmaytac | Assigned To | => correnson | ||
2018-10-01 10:01 | jmaytac | File Added: framaBug.tar.gz | |||
2018-10-02 00:39 | jmaytac | Note Added: 0006650 | |||
2018-10-02 00:40 | jmaytac | File Added: frmaBug.tar.gz | |||
2018-10-02 08:36 | virgile | Relationship added | has duplicate 0002403 | ||
2018-10-02 08:40 | virgile | View Status | private => public | ||
2018-10-02 10:43 | correnson | Note Added: 0006653 | |||
2018-10-02 10:44 | correnson | Note Edited: 0006653 | bug_revision_view_page.php?bugnote_id=6653#r362 | ||
2018-10-02 10:44 | correnson | Note Added: 0006654 | |||
2018-10-02 10:44 | correnson | Status | assigned => acknowledged | ||
2018-10-02 10:45 | correnson | Note Added: 0006655 | |||
2019-10-17 17:07 | correnson | Status | acknowledged => resolved | ||
2019-10-17 17:07 | correnson | Resolution | open => no change required | ||
2019-10-17 18:00 | signoles | Status | resolved => closed |