Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002403Frama-CPlug-in > wppublic2018-10-01 22:512018-10-02 08:36
Reporterjmaytac 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionduplicate 
PlatformOSOS Version
Product VersionFrama-C 17-Chlorine 
Target VersionFixed in Version 
Summary0002403: Newer releases of FramaC produce apparent WP plug-in bug
DescriptionThe 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.
Steps To Reproducetar -xvf framaBug.tar.gz
make wp
TagsNo tags attached.
Attached Filesgz file icon framaBug.tar.gz [^] (383,447 bytes) 2018-10-01 22:51
gz file icon frmaBug.tar.gz [^] (140,283 bytes) 2018-10-02 05:50

- Relationships
duplicate of 0002401acknowledgedcorrenson Newer releases of FramaC produce apparent WP plug-in bug 

-  Notes
(0006651)
jmaytac (reporter)
2018-10-02 05:51
edited on: 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 (developer)
2018-10-02 08:34

This seems to be the exact same bug as 0002401.

- Issue History
Date Modified Username Field Change
2018-10-01 22:51 jmaytac New Issue
2018-10-01 22:51 jmaytac Status new => assigned
2018-10-01 22:51 jmaytac Assigned To => correnson
2018-10-01 22:51 jmaytac File Added: framaBug.tar.gz
2018-10-02 05:50 jmaytac File Added: frmaBug.tar.gz
2018-10-02 05:51 jmaytac Note Added: 0006651
2018-10-02 05:51 jmaytac Note Edited: 0006651 View Revisions
2018-10-02 08:34 virgile Note Added: 0006652
2018-10-02 08:36 virgile Status assigned => closed
2018-10-02 08:36 virgile Resolution open => duplicate
2018-10-02 08:36 virgile Relationship added duplicate of 0002401


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker