Frama-C-discuss mailing list archives

loic.correnson at cea.fr (Loïc Correnson) · Wed, 5 Nov 2014 15:06:15 +0100

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.
	L.

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

> 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
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

Frama-C-discuss mailing list archives

[Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow