Frama-C Bug Tracking System - Frama-C |
| View Issue Details |
|
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0002401 | Frama-C | Plug-in > wp | public | 2018-10-01 10:01 | 2019-10-17 18:00 |
|
| Reporter | jmaytac | |
| Assigned To | correnson | |
| Priority | normal | Severity | major | Reproducibility | always |
| Status | closed | Resolution | no change required | |
| Platform | | OS | | OS Version | |
| Product Version | Frama-C 17-Chlorine | |
| Target Version | | Fixed in Version | | |
|
| Summary | 0002401: Newer releases of FramaC produce apparent WP plug-in bug |
| Description | 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.
|
| Steps To Reproduce | tar -xvf framaBug.tar.gz
make wp |
| Additional Information | |
| Tags | No tags attached. |
| Relationships | | has duplicate | 0002403 | closed | correnson | Newer releases of FramaC produce apparent WP plug-in bug |
|
| Attached Files |  framaBug.tar.gz (383,447) 2018-10-01 10:01
https://bts.frama-c.com/file_download.php?file_id=1284&type=bug
frmaBug.tar.gz (140,283) 2018-10-02 00:40
https://bts.frama-c.com/file_download.php?file_id=1286&type=bug |
|
| 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 |
|
Notes |
|
|
|
|
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
|
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!
|
|
|
|
|
|
Frama-C / WP shall properly detect and reject access to volatile locations inside body of logic function and predicates. |
|
|
|
|
|
Workaround: you can use -wp-no-volatile option to (inconsistently) ignore all volatile flags. |
|