Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] strlen axioms and memory space
  • From: efremov at ispras.ru (Denis Efremov)
  • Date: Fri, 31 Jul 2020 01:04:37 +0300
  • In-reply-to: <CA+RLCQxBYXp=scYivpatSUhNQYV+XPzzb=Rbrys=TKcRkORuCg@mail.gmail.com>
  • References: <CA+RLCQx4DaVUCrK__=ocAXYMzKrzCtQcxoc9eMfgV6i3JuXVXw@mail.gmail.com> <e396e52b-52dd-8db6-7bcc-957962ec2aec@ispras.ru> <CA+RLCQxBYXp=scYivpatSUhNQYV+XPzzb=Rbrys=TKcRkORuCg@mail.gmail.com>
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