Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002401Frama-CPlug-in > wppublic2018-10-01 10:012018-10-02 10:45
Reporterjmaytac 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusacknowledgedResolutionopen 
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.
Attached Filesgz file icon framaBug.tar.gz [^] (383,447 bytes) 2018-10-01 10:01
gz file icon frmaBug.tar.gz [^] (140,283 bytes) 2018-10-02 00:40

- Relationships
has duplicate 0002403closedcorrenson Newer releases of FramaC produce apparent WP plug-in bug 

-  Notes
(0006650)
jmaytac (reporter)
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)
(0006653)
correnson (manager)
2018-10-02 10:43
edited on: 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!

(0006654)
correnson (manager)
2018-10-02 10:44

Frama-C / WP shall properly detect and reject access to volatile locations inside body of logic function and predicates.
(0006655)
correnson (manager)
2018-10-02 10:45

Workaround: you can use -wp-no-volatile option to (inconsistently) ignore all volatile flags.

- Issue History
Date Modified Username Field Change
2018-10-01 10:01 jmaytac New Issue
2018-10-01 10:01 jmaytac Status new => assigned
2018-10-01 10:01 jmaytac Assigned To => correnson
2018-10-01 10:01 jmaytac File Added: framaBug.tar.gz
2018-10-02 00:39 jmaytac Note Added: 0006650
2018-10-02 00:40 jmaytac File Added: frmaBug.tar.gz
2018-10-02 08:36 virgile Relationship added has duplicate 0002403
2018-10-02 08:40 virgile View Status private => public
2018-10-02 10:43 correnson Note Added: 0006653
2018-10-02 10:44 correnson Note Edited: 0006653 View Revisions
2018-10-02 10:44 correnson Note Added: 0006654
2018-10-02 10:44 correnson Status assigned => acknowledged
2018-10-02 10:45 correnson Note Added: 0006655


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker