2021-01-15 18:47 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002401Frama-CPlug-in > wppublic2019-10-17 18:00
Reporterjmaytac 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionno change required 
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 Files

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

-Notes

~0006650

jmaytac (reporter)

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)

Last edited: 2018-10-02 10:44

View 2 revisions

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)

Frama-C / WP shall properly detect and reject access to volatile locations inside body of logic function and predicates.

~0006655

correnson (manager)

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

-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
2019-10-17 17:07 correnson Status acknowledged => resolved
2019-10-17 17:07 correnson Resolution open => no change required
2019-10-17 18:00 signoles Status resolved => closed
+Issue History