specification for library functions?

Jun 6, 2014 at 8:17 AM
I wonder whether there is a VCC specification for common library functions such as strlen. The lack of this has been one of key obstacles when using a static verification tool such as VCC, and I wonder how serious this problem is in the case of VCC. Thanks.
Aug 26, 2014 at 3:11 AM
it's not possible , i think. because we can't change the c standard header files and if we write the contracts on a separated header file causes the "ambiguouse call " Error since there will be two files with the same function name.