--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on July 2020 ---
On 7/31/20 12:50 AM, Yurii Rashkovskii wrote: > Hi Denis, > > Your link actually leads to even more "interesting" thoughts. My axiom stated that any strlen should be less or equal than UINTPTR_MAX. But assuming that strings s1 and s2 are not overlapping, the sum of their lengths is seemingly less or equal than UINTPTR_MAX. Well, I express strlen as (https://github.com/evdenis/verker/blob/master/src/strlen.h#L84-L85) Â Â Â logic size_t strlen(char *s) = Â Â Â Â Â Â s[0] == '\0' ? (size_t) 0 : (size_t) ((size_t)1 + strlen(s + 1)); and I hope that this definition is not self-contradictionary. There were "fears" that it's possible to deduce a contradiction from an "increasing" logic function that returns a bounded type. However, we didn't face it with Jessie plugin. It's easy to shoot yourself in the foot with something like these: https://bts.frama-c.com/view.php?id=2427 https://bts.frama-c.com/view.php?id=2338 Regards, Denis