Frama-C Bug Tracking System - Frama-C
View Issue Details
0002403Frama-CPlug-in > wppublic2018-10-01 22:512018-10-02 08:36
jmaytac 
correnson 
normalmajoralways
closedduplicate 
Frama-C 17-Chlorine 
 
0002403: Newer releases of FramaC produce apparent WP plug-in bug
The attached code base is a small example in which a reactive program interacts with peripherals via memory mapped I/O through a constant address. While earlier releases of framaC (Phosphorous) was able to generate full and faithful altergo for our proofs, the new version produces syntactically malformed altergo for the following boolean logic function defined in our example's ACSL: mac.h line 35: logic boolean isAMessage(mac_t mac) = ((mac->mac_packet.object_high == 0x0A) && (mac->mac_\ packet.object_low == 0x0A) && (mac->mac_packet.payload_length == 0x00)); Whereas such boolean logic functions were correctly axiomatized in the older (Phosphorous) release, the current version is axiomatizing such a function as : function L_isAMessage () : bool = andb(eqb(#{w_0}, 0), andb(eqb(#{w_1}, 10), eqb(#{w_2}, 10))) note that the argument to the logic function is absent, and the fields of hte mac_t referenced in the logic function are rendered as "#{w_i}", about which altergo then complains. These malformed altergo expressions seem to have been generated by the pretty printer's find_var function.
tar -xvf framaBug.tar.gz make wp
No tags attached.
duplicate of 0002401closed correnson Newer releases of FramaC produce apparent WP plug-in bug 
gz framaBug.tar.gz (383,447) 2018-10-01 22:51
https://bts.frama-c.com/file_download.php?file_id=1285&type=bug
gz frmaBug.tar.gz (140,283) 2018-10-02 05:50
https://bts.frama-c.com/file_download.php?file_id=1287&type=bug
Issue History
2018-10-01 22:51jmaytacNew Issue
2018-10-01 22:51jmaytacStatusnew => assigned
2018-10-01 22:51jmaytacAssigned To => correnson
2018-10-01 22:51jmaytacFile Added: framaBug.tar.gz
2018-10-02 05:50jmaytacFile Added: frmaBug.tar.gz
2018-10-02 05:51jmaytacNote Added: 0006651
2018-10-02 05:51jmaytacNote Edited: 0006651View Revisions
2018-10-02 08:34virgileNote Added: 0006652
2018-10-02 08:36virgileStatusassigned => closed
2018-10-02 08:36virgileResolutionopen => duplicate
2018-10-02 08:36virgileRelationship addedduplicate of 0002401

Notes
(0006651)
jmaytac   
2018-10-02 05:51   
We've attached just now an even smaller example (frmaBug.tar.gz as opposed to framaBug.tar.gz) producing the bug, where the ACSL definition of the involved logic function is to be found on line 21 of mac.h /*@ logic boolean isAMessage(mac_t mac) = (mac->mac_packet.object_high == 0x0A); */ and the altergo produced is on line 5 of Axiomatic11.ergo function L_isAMessage() : bool = eqb(#{w_0}, 10)
(0006652)
virgile   
2018-10-02 08:34   
This seems to be the exact same bug as #2401.