Frama-C Bug Tracking System - Frama-C
View Issue Details
0002401Frama-CPlug-in > wppublic2018-10-01 10:012019-10-17 18:00
Assigned Tocorrenson 
StatusclosedResolutionno change required 
PlatformOSOS Version
Product VersionFrama-C 17-Chlorine 
Target VersionFixed in Version 
Summary0002401: Newer releases of FramaC produce apparent WP plug-in bug
DescriptionThe 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 Reproducetar -xvf framaBug.tar.gz
make wp
TagsNo tags attached.
has duplicate 0002403closed correnson Newer releases of FramaC produce apparent WP plug-in bug 
Attached Filesgz framaBug.tar.gz (383,447) 2018-10-01 10:01
gz frmaBug.tar.gz (140,283) 2018-10-02 00:40

2018-10-02 00:39   
We've attached just now an even smaller example 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)
2018-10-02 10:43   
(Last edited: 2018-10-02 10:44)
After *much further reduction* the bug can be reduced to:

/* Generated by Frama-C */

typedef struct {
   unsigned char object_high ;
} mac_packet_t ;

typedef struct mac {
  mac_packet_t volatile mac_packet ;
} *mac_t;

logic 𝔹 isAMessage{L}(mac_t mac) =
  \at(mac->mac_packet.object_high ≡ 0x0A,L);

/*@ behavior NO:
      assumes mac->mac_packet.object_high ≢ 0x0A;
    behavior A:
      assumes isAMessage(mac) ≡ \true;
    complete behaviors A, NO;
    disjoint behaviors A, NO;
int mac_getBusMsg(mac_t mac)
  return 0;

The problem comes from the **volatile** field of structure mac, which is read from a logic function.

Reading something volatile inside a logic term has absolutely *NO* concrete meaning in ACSL.
The WP generates fresh variables (aka: random values) when accessing volatiles from logic, in an attempt of remaining consistent. This strategy fails when being inside a logic function body since those variables escape any definition scope.

In previous versions of Frama-C/WP, accessing volatiles inside logic was silently accepted with an inconsistent semantics ;-)

However, I agree that such such a situation shall be detected with a more user-friendly error message!

2018-10-02 10:44   
Frama-C / WP shall properly detect and reject access to volatile locations inside body of logic function and predicates.
2018-10-02 10:45   
Workaround: you can use -wp-no-volatile option to (inconsistently) ignore all volatile flags.

Issue History
2018-10-01 10:01jmaytacNew Issue
2018-10-01 10:01jmaytacStatusnew => assigned
2018-10-01 10:01jmaytacAssigned To => correnson
2018-10-01 10:01jmaytacFile Added: framaBug.tar.gz
2018-10-02 00:39jmaytacNote Added: 0006650
2018-10-02 00:40jmaytacFile Added: frmaBug.tar.gz
2018-10-02 08:36virgileRelationship addedhas duplicate 0002403
2018-10-02 08:40virgileView Statusprivate => public
2018-10-02 10:43corrensonNote Added: 0006653
2018-10-02 10:44corrensonNote Edited: 0006653bug_revision_view_page.php?bugnote_id=6653#r362
2018-10-02 10:44corrensonNote Added: 0006654
2018-10-02 10:44corrensonStatusassigned => acknowledged
2018-10-02 10:45corrensonNote Added: 0006655
2019-10-17 17:07corrensonStatusacknowledged => resolved
2019-10-17 17:07corrensonResolutionopen => no change required
2019-10-17 18:00signolesStatusresolved => closed