Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • 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
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #241
Closed
Open
Issue created Oct 01, 2018 by mantis-gitlab-migration@mantis-gitlab-migration

Newer releases of FramaC produce apparent WP plug-in bug

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


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

Description :

The attached code base is a small example in which a reactive program interacts with peripherals via memory mapped I/O through a constant address. While earlier releases of framaC (Phosphorous) was able to generate full and faithful altergo for our proofs, the new version produces syntactically malformed altergo for the following boolean logic function defined in our example's ACSL: mac.h line 35: logic boolean isAMessage(mac_t mac) = ((mac->mac_packet.object_high == 0x0A) && (mac->mac_
packet.object_low == 0x0A) && (mac->mac_packet.payload_length == 0x00));

Whereas such boolean logic functions were correctly axiomatized in the older (Phosphorous) release, the current version is axiomatizing such a function as : function L_isAMessage () : bool = andb(eqb(#{w_0}, 0), andb(eqb(#{w_1}, 10), eqb(#{w_2}, 10)))

note that the argument to the logic function is absent, and the fields of hte mac_t referenced in the logic function are rendered as "#{w_i}", about which altergo then complains. These malformed altergo expressions seem to have been generated by the pretty printer's find_var function.

Steps To Reproduce :

tar -xvf framaBug.tar.gz make wp

Attachments

  • framaBug.tar.gz
  • frmaBug.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