Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002407Frama-CPlug-in > wppublic2018-10-31 02:302019-10-17 17:59
Reporterjmaytac 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C 17-Chlorine 
Target VersionFixed in Version 
Summary0002407: contracts about memory mapped I/O through volatile memory locations
DescriptionWe've attached a small example in which a state machine communicates a peripheral through a volatile variable , on line 6 of constants.h: volatile uint32_t rxBuffer; The state of the machine is held by a struct mac, declared on line 21 of mac.h: struct mac { mac_packet_t mac_packet; MessageType latestMessage; mac_bridge_t MAC_BRIDGE_A; } the mac_bridge_t represents the machine's memory mapped I/O interface, as declared on line 15 of mac_bridge.h: struct mac_bridge { volatile uint32_t *cmd_rx_buffer; } on line 13 of main.c, mac_t mac = the_mac(); mac becomes a pointer to singleton_mac instance of struct mac declared on line 8 of mac.c and returned by the function the_mac() defined on line 17 of mac.c. On line 14 of main.c, mac->MAC_BRIDGE_A = theMacBridge(); mac's IO interface MAC_BRIDGE_A becomes the singletonMacBridgeA instance of struct mac_bridge returned by the function theMacBridge() defined on line 11 of mac.c mac_bridge_t theMacBridge() { singletonMacBridgeA.cmd_rx_buffer = &rxBuffer; return &singletonMacBridgeA; } thus, mac has as MAC_BRIDGE_A singletonMacBridgeA whose cmd_rx_buffer is a reference to the volatile rxBuffer. The volatile rxBuffer reads and writes from ghost state as given on line 7 of constants.h: //@ ghost uint32_t injectorAPBBuffer[4294967296]; //@ ghost uint32_t injectorAPBBufferCount=0; /*@ ghost //@ requires buffer == &(rxBuffer); @ uint32_t readsBuffer(volatile uint32_t *buffer) { @ static uint32_t injectorAPBBufferCount = 0; @ for (int i=0; i<4294967296; i++) { @ injectorAPBBuffer[i%4294967296]=i%42949967296; @ } @ if (buffer == &(rxBuffer)) { @ return injectorAPBBuffer[injectorAPBBufferCount++]; @ } @ else @ return 0; @ } @ */ //@ ghost uint32_t bufferAPBCollector[4294967296]; //@ ghost uint32_t bufferAPBCollectorCount = 0; /*@ ghost //@ requires buffer == &(rxBuffer); @ uint32_t writesBuffer(volatile uint32_t *buffer, uint32_t v) { @ if (buffer == &(rxBuffer)){ @ return bufferAPBCollector[(bufferAPBCollectorCount++)%64] = v; @ } @ else { @ return 0; @ } @ } @*/ //@ volatile (rxBuffer) reads readsBuffer writes writesBuffer; mac implements a transition system driven by an alphabet of labels obtained through calls to macbridge_get_packet, defined on line 3 of mac_bridge.c mac_packet_t macbridge_get_packet(mac_bridge_t mac_bridge) { mac_packet_t received_packet={0}; received_packet.object_high=(uint8_t)(*(mac_bridge->cmd_rx_buffer)); return(received_packet); } when the given macbridge_t is the reference to the singletonMacBridgeA, we want this function to have as postcondition that the packet this function returns has the value found in the appropriate ghost state /*@ behavior A: assumes mac_bridge == &singletonMacBridgeA; ensures \result.object_high == (uint8_t)injectorAPBBuffer[(injectorAPBBufferCount-1)%4294967296]; */ mac_packet_t macbridge_get_packet(mac_bridge_t mac_bridge); The resulting Alt-ergo doesn't seem to capture the post-condition. (* ---------------------------------------------------------- *) (* --- Post-condition (file mac_bridge.h, line 24) in 'macbridge_get_packet' --- *) (* ---------------------------------------------------------- *) goal macbridge_get_packet_post: forall t : int farray. forall t_1 : (addr,int) farray. forall t_2 : (addr,addr) farray. forall a : addr. let a_1 = shiftfield_F7_mac_bridge_cmd_rx_buffer(a) : addr in let a_2 = t_2[a_1] : addr in let x = t_1[a_2] : int in (region(a.base) <= 0) -> framed(t_2) -> linked(t) -> valid_rd(t, a_1, 1) -> is_uint32(x) -> valid_rd(t, a_2, 1) -> (x = to_uint8(x))
TagsNo tags attached.
Attached Filesgz file icon framaExample.tar.gz [^] (2,585 bytes) 2018-10-31 02:30

- Relationships

-  Notes
(0006675)
correnson (manager)
2018-10-31 14:50

Your approach in using explicit volatile reads & writes clauses is good one. However, without using the Volatile plug-in, these clauses are _not_ taken into account by Frama-C kernel, and access to volatile memories simply leads to introduce random values (aka: fresh variables) into the proof obligations. The Volatile plug-in is not part of the open-source distribution. Please contact us for dedicated support if you need so.
(0006900)
correnson (manager)
2019-10-17 16:56

The (non-free) volatile plug-in must be used to instrument this kind of code.

- Issue History
Date Modified Username Field Change
2018-10-31 02:30 jmaytac New Issue
2018-10-31 02:30 jmaytac Status new => assigned
2018-10-31 02:30 jmaytac Assigned To => correnson
2018-10-31 02:30 jmaytac File Added: framaExample.tar.gz
2018-10-31 14:50 correnson Note Added: 0006675
2019-10-17 16:56 correnson Note Added: 0006900
2019-10-17 16:56 correnson Status assigned => resolved
2019-10-17 16:56 correnson Resolution open => fixed
2019-10-17 17:59 signoles Status resolved => closed


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker