Skip to content

GitLab

  • Menu
Projects Groups 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
    • 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
  • #644

Closed
Open
Created May 04, 2015 by Jochen Burghardt@burghardt

different signatures for "linked" in definition and use in generated Alt-Ergo mlw file

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


Id Project Category View Due Date Updated
ID0002111 Frama-Clang Plug-in > clang public 2015-05-04 2015-05-04
Reporter Jochen Assigned To virgile Resolution open
Priority normal Severity minor Reproducibility always
Platform Sodium-20150201 OS - OS Version xubuntu14.04
Product Version Frama-C Sodium Target Version - Fixed in Version -

Description :

Running "frama-c -wp -wp-rte -wp-out wp-out 475.cpp" generated the file "_Z3fooR1X_assert_rte_mem_access_Alt-Ergo.mlw" which seems to contain different signatures of "linked":

... 493 logic linked : (int,int) farray -> prop ... 766 forall t : int farray. 767 forall t_1 : (addr,int) farray. 768 forall a : addr. 769 let a_1 = shiftfield_F__Z1X_x(a) : addr in 770 linked(t) -> ...

"linked" is declared as taking an argument of type "(int,int) farray", but at its single use it is given an argument of type "int farray".

I'm not sure whether this is ok (maybe Alt-Ergo provides overloading?) or indicates an error. Alt-Ergo doesn't complain, anyway.

Attachments

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