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] Arbitrary size fixed integer math

  • Subject: [Frama-c-discuss] Arbitrary size fixed integer math
  • From: kurt at roeckx.be (Kurt Roeckx)
  • Date: Sat, 24 Oct 2015 14:04:30 +0200
Hi,

I was wondering if it would be possible to verify the math of the
BN library in OpenSSL. So I tried a little test program to see
what would happen. I was actually kind of expecting it not to
work, and it seems to be unable to prove it.

Is this something I should be able to get working?

I've attached a simple test program I was trying with.


Kurt

-------------- next part --------------
A non-text attachment was scrubbed...
Name: bn_add.c
Type: text/x-csrc
Size: 1761 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20151024/2eba9282/attachment.c>