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.