0002403: Newer releases of FramaC produce apparent WP plug-in bug

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002403

Frama-C

Plug-in > wp

public

2018-10-01 22:51

2018-10-02 08:36

Reporter

jmaytac

Assigned To

correnson

Priority

normal

Severity

major

Reproducibility

always

Status

closed

Resolution

duplicate

Platform

OS Version

Product Version

Frama-C 17 Chlorine

Target Version

Fixed in Version

Summary

0002403: Newer releases of FramaC produce apparent WP plug-in bug

Description

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.

Steps To Reproduce

tar -xvf framaBug.tar.gz
make wp

Tags

No tags attached.

Attached Files

framaBug.tar.gz [^] (383,447 bytes) 2018-10-01 22:51

frmaBug.tar.gz [^] (140,283 bytes) 2018-10-02 05:50

Relationships

duplicate of

0002401

acknowledged

correnson

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