--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on July 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] strlen axioms and memory space



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