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.