# 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

*Subject*: [Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow*From*: virgile.prevosto at m4x.org (Virgile Prevosto)*Date*: Tue, 4 Nov 2014 10:01:51 +0100*In-reply-to*: <CAAS2fgRTEAODJ78tg7m77oDEyK4XG0E0GHLRkrqm7tRNFwY3bg@mail.gmail.com>*References*: <CAAS2fgRTEAODJ78tg7m77oDEyK4XG0E0GHLRkrqm7tRNFwY3bg@mail.gmail.com>

Hello, 2014-11-04 0:14 GMT+01:00 Gregory Maxwell <gmaxwell at gmail.com>: > > To start with, I need to first prove that the code is overflow free, > under assumptions. (I don't just need to do this to make WP happy, its > required for correctness of the code. > > Here is a reduced testcase that I'm trying: > > $ cat a.c > #include <stdint.h> > void static inline secp256k1_fe_mul_inner(const uint32_t *a, const > uint32_t *b, uint32_t *r) { > uint64_t d; > d = (uint64_t)a[0] * b[9] > > frama-c -main secp256k1_fe_mul_inner -lib-entry -wp -wp-timeout 300 > -wp-par 1 -wp-rte a.c > First of all, I'd say that for checking potential overflows in this context, Value Analysis could do the trick at least as easily as WP. The command line would be like this: frama-c -main secp256k1_fe_mul_inner -lib-entry -val overflow.c -context-width 10 -context-valid-pointers -warn-unsigned-overflow The extra arguments indicate - that your pointers a and b are valid (-context-valid-pointers) - that they point to blocks of size 10 (-context-width 10) - and that you want to be warned when an unsigned arithmetic operation may overflow (-warn-unsigned-overflow). Indeed, as unsigned overflows (contrarily to signed overflows) are well defined by the standard, by default Value do not report alarms on them. If you launch this command, you'll see a lot of alarms like this: overflow.c:28:[kernel] warning: unsigned overflow. assert (unsigned long)*(a+0)*(unsigned long)*(b+9) ? 4294967295; The culprit here is #include <stdint.h>: by default, this will use your system's headers, which are unlikely to be consistent with Frama-C's default machdep x86_32. In other words, the typedef you have in /usr/include/stdint.h for uint64_t will end up in an integral type interpreted as 32 bit by Frama-C, hence the alarms. In order to have headers that match your machdep, you have to instruct the external preprocessor to use Frama-C's standard headers (and if you don't use the default machdep, you also have to define the appropriate macro as seen in FRAMAC_SHARE/libc/__fc_machdep.h). This is done in the following command line: frama-c -main secp256k1_fe_mul_inner -lib-entry -val overflow.c -context-width 10 -context-valid-pointers -warn-unsigned-overflow -cpp-extra-args="-I$(frama-c -print-share-path)/libc" I agree that this is error-prone. The next version of Frama-C is likely to use Frama-C's own standard headers, and pass to the pre-processor the -D option that corresponds to the selected machdep. This should be less confusing. Best regards, -- E tutto per oggi, a la prossima volta Virgile

**Follow-Ups**:**[Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow***From:*gmaxwell at gmail.com (Gregory Maxwell)

**[Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow***From:*loic.correnson at cea.fr (Loïc Correnson)

**References**:**[Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow***From:*gmaxwell at gmail.com (Gregory Maxwell)

- Prev by Date:
**[Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow** - Next by Date:
**[Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow** - Previous by thread:
**[Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow** - Next by thread:
**[Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow** - Index(es):