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