ID0002401: **This issue was created automatically from Mantis Issue 2401. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002401 | Frama-C | Plug-in > wp | public | 2018-10-01 | 2019-10-17 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | jmaytac | **Assigned To** | correnson | **Resolution** | no change required | | **Priority** | normal | **Severity** | major | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - | ### 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 ## Attachments - [framaBug.tar.gz](/uploads/f07e549fb7296718c7ae0d86fb99b96e/framaBug.tar.gz) - [frmaBug.tar.gz](/uploads/a43835306fcfcff1aef5bd28e09e0b4d/frmaBug.tar.gz)