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
  • #601

Closed
Open
Created Aug 31, 2015 by Jochen Burghardt@burghardt

bound variable names in Coq file depend on unrelated function later in C source code

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


Id Project Category View Due Date Updated
ID0002153 Frama-C Plug-in > wp public 2015-08-31 2015-09-03
Reporter Jochen Assigned To correnson 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 -pp-annot -wp -wp-split -kernel-msg-key pp -wp-model Typed+ref -wp-driver ../BitTest.driver -cpp-command 'gcc -C -E' -wp-timeout 2 -wp-coq-timeout 5 -wp-prover cvc4 -wp-prover coq 0.c -wp-out 0.wp" on the attached file "0.c", and the corresponding command on "1.c", generate Coq proof obligation files "0.wp/typed_ref_BitTest/Bitstream_WriteThenRead_assert_left.coq" and "1.wp/typed_ref_BitTest/Bitstream_WriteThenRead_assert_left.coq" that differ in bound variable names.

However, "0.c" initially just includes "1.c" and the defines a function "Bitstream_ReadThenWrite" that is unrelated to the code in "1.c"; for this reason, it shouldn't influence the proof obligation of "Bitstream_WriteThenRead_assert_left". The influence apparently depends on the name of the trailing extra-function in "0.c": if it is named "Bitstream_XeadThenWrite", then the problem disappears. Frama-C handles functions in alphabetical order, as can be seen by its stdout messages.

Attachments

  • 0.c
  • 1.c
  • BitTest.driver
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking