Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #117

Closed
Open
Created Oct 31, 2018 by mantis-gitlab-migration@mantis-gitlab-migration

contracts about memory mapped I/O through volatile memory locations

ID0002407: This issue was created automatically from Mantis Issue 2407. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0002407 Frama-C Plug-in > wp public 2018-10-31 2019-10-17
Reporter jmaytac Assigned To correnson Resolution fixed
Priority normal Severity major Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C 17-Chlorine Target Version - Fixed in Version -

Description :

We'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))

Attachments

  • framaExample.tar.gz
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking