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
  • #885
Closed
Open
Issue created Jan 05, 2015 by Jochen Burghardt@burghardt

constructor overloading resolution with templates causes dubious "contract merge" warning

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


Id Project Category View Due Date Updated
ID0002043 Frama-Clang Plug-in > clang public 2015-01-05 2015-02-15
Reporter Jochen Assigned To virgile Resolution open
Priority normal Severity minor Reproducibility always
Platform frama-c-Neon-20140301+dev-stance OS - OS Version xubuntu-cfe13.10
Product Version - Target Version - Fixed in Version -

Description :

Running "frama-c -wp 426.cpp" produces the output:

Now output intermediate result 426.cpp:5:[kernel] warning: found two contracts. Merging them [wp] Running WP plugin...

The warning remains if (1) the contract in line 7 is activated, or (2) the contract in line 11 is deactivated.

The warning disappears if (3) lines 4-5 are deleted, (4) line 8 is deleted, or (5) "char" is changed to "int" in line 13.

Even if the warning is printed, the proof obligation for the constructor call in line 13 seems to be correct, viz.:

(* ---------------------------------------------------------- ) ( --- Instance of 'Pre-condition (file 426.cpp, line 4) in '_ZN7complexIcEEC1vci'' in 'main' at call '_ZN7complexIcEEC1vci' (file 426.cpp, line 13) --- ) ( ---------------------------------------------------------- *)

goal main_call__ZN7complexIcEEC1vci_pre: forall i : int. forall t : int farray. (i <= 6) -> linked(t) -> is_sint32(i) -> (1 = i)

So it is not clear which contracts are merged. Possibly this is a revival of issue #1611. However, it could also indicate that the contract in line 4 is merged with the (empty) contract of the constructor in line 8 (since the warning disappears when line 8 is removed) - which would be wrong in general.

Attachments

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