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] WP failing to prove a simple absence of RTE unsigned overflow

Hi!

On Tue, Nov 4, 2014 at 10:24 AM, Gregory Maxwell <gmaxwell at gmail.com> wrote:

> With your help value analysis works great now, and on the whole function.


In another forum, but on the same topic, you wrote:

"sadly, frama-c doesn't support the __int128, alas."

Adding a new basic integer type to Frama-C's front-end would be
no picnic and I cannot recommend it.

On the other hand, if you want to experiment, in the spirit of Open-Source,
I should point out that you could use "long long int" for 128-bit,
which would still leave you "long int" for 64-bit and "int" for 32-bit.

The file to experiment with is cil/src/machdeps.ml. It relates to
the commandline option -machdep. If this destroys
your harddrive, I will disavow any knowledge of your actions,
but I, and maybe others, would be curious about the results if you
try it.

Pascal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141105/6991c082/attachment.html>