Frama-C Bug Tracking System - Frama-C
View Issue Details
0002401Frama-CPlug-in > wppublic2018-10-01 10:012019-10-17 18:00
closedno change required 
Frama-C 17-Chlorine 
0002401: Newer releases of FramaC produce apparent WP plug-in bug
The 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.
tar -xvf framaBug.tar.gz make wp
No tags attached.
has duplicate 0002403closed correnson Newer releases of FramaC produce apparent WP plug-in bug 
gz framaBug.tar.gz (383,447) 2018-10-01 10:01
gz frmaBug.tar.gz (140,283) 2018-10-02 00:40
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: 0006653View Revisions
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

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   
(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!
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.