--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on November 2014 ---
Probably the same problem as http://lists.gforge.inria.fr/pipermail/why-discuss/2014-October/000697.html You should run fram-c with extra option: -cpp-extra-args="-I$(frama-c -print-share-path)/libc" - Claude Le 04/11/2014 00:14, Gregory Maxwell a ?crit : > Greetings, I haven't used frama-c in some time, it's changed quite a > bit (and I've likely forgotten even more...) and I'm having a hard > time making progress with it at all this time around. > > I'm working on libsecp256k1 a free software cryptographic signature > library which will be used by the reference Bitcoin software; > verifying that optimized implementations are exactly correct is > critical for this application > > I'm trying to prove some simple theorems about some inner kernels used > for field arithmetic. > > 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> > /*@ requires \valid(a + (0..9)); > requires \valid(b + (0..9)); > requires (a[0] < 1073741824); > requires (a[1] < 1073741824); > requires (a[2] < 1073741824); > requires (a[3] < 1073741824); > requires (a[4] < 1073741824); > requires (a[5] < 1073741824); > requires (a[6] < 1073741824); > requires (a[7] < 1073741824); > requires (a[8] < 1073741824); > requires (a[9] < 67108864); > requires (b[0] < 1073741824); > requires (b[1] < 1073741824); > requires (b[2] < 1073741824); > requires (b[3] < 1073741824); > requires (b[4] < 1073741824); > requires (b[5] < 1073741824); > requires (b[6] < 1073741824); > requires (b[7] < 1073741824); > requires (b[8] < 1073741824); > requires (b[9] < 67108864); > */ > 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] > + (uint64_t)a[1] * b[8] > + (uint64_t)a[2] * b[7] > + (uint64_t)a[3] * b[6] > + (uint64_t)a[4] * b[5] > + (uint64_t)a[5] * b[4] > + (uint64_t)a[6] * b[3] > + (uint64_t)a[7] * b[2] > + (uint64_t)a[8] * b[1] > + (uint64_t)a[9] * b[0]; > } > > I invoke frama-c with: > > frama-c -main secp256k1_fe_mul_inner -lib-entry -wp -wp-timeout 300 > -wp-par 1 -wp-rte a.c > > And get some successful proof for memory access, followed by alt-ergo > returning unknown on the overflow checks: > [...] > [wp] [Alt-Ergo] Goal > typed_secp256k1_fe_mul_inner_assert_rte_mem_access_20 : Valid > (Qed:1ms) (93ms) (74) > [wp] [Alt-Ergo] Goal > typed_secp256k1_fe_mul_inner_assert_rte_unsigned_overflow : Unknown > (Qed:4ms) (4s) > [wp] [Alt-Ergo] Goal > typed_secp256k1_fe_mul_inner_assert_rte_unsigned_overflow_2 : Unknown > (Qed:5ms) (4s) > > This is obviously free of overflows, since 1073741824*1073741824*8 + > 1073741824*67108864*2 < 2^64 > > (but the non-reduced code, is less trivial > http://0bin.net/paste/tTR7910ESfwij7Ib#pZwnZkivigEp+73f4D4yWQpXMaEWCmVFTb4XxE6vRUN > ... which is why I'm starting with just proving overflows since the > hand verifiable correctness proof in the comments assumes no > overflow). > > I'm using alt-ergo 0.95.1 and frama-c Neon-20140301 > > Any suggestions? > _______________________________________________ > 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 > -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |