--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on November 2014 ---
[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>