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: loic.correnson at (Loïc Correnson)
  • Date: Wed, 5 Nov 2014 15:06:15 +0100
  • In-reply-to: <>
  • References: <> <>

Yes, Value is more suitable for proving the absence of runtime errors than WP.
Especially, as far as we know, Alt-Ergo is sometimes confused by the large constants (2^32, ?) involved when proving absence of overflows.

Le 4 nov. 2014 ? 10:01, Virgile Prevosto <virgile.prevosto at> a ?crit :

> Hello,
> 2014-11-04 0:14 GMT+01:00 Gregory Maxwell <gmaxwell at>:
>> 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
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at