--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on December 2014 ---
Hello, Le 12/12/2014 08:22, Roberto Bagnara a ?crit : > Apparently the latest version > of Frama-C is not able to prove that a nonzero unsigned quantity > shifted to the right by a nonzero number of positions results > in a strict decrease. Frama-C is known to be weak on bit-related operations. It has been told on this list that this part is under work. > Replacing shift by integer division does > not help. This is strange. On attached example, the variant with a division is proved without any issue. """ $ frama-c -wp shift-variant.c [kernel] preprocessing with "gcc -C -E -I. shift-variant.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards shift-variant.c:9:[wp] warning: Missing assigns clause (assigns 'everything' instead) shift-variant.c:23:[wp] warning: Missing assigns clause (assigns 'everything' instead) [wp] 4 goals scheduled [wp] [Alt-Ergo] Goal typed_testVariant_div_loop_term_positive : Valid (12ms) (4) [wp] [Alt-Ergo] Goal typed_testVariant_div_loop_term_decrease : Valid (20ms) (10) [wp] [Alt-Ergo] Goal typed_testVariant_loop_term_positive : Valid (15ms) (4) [wp] [Alt-Ergo] Goal typed_testVariant_loop_term_decrease : Unknown [wp] Proved goals: 3 / 4 Qed: 0 Alt-Ergo: 3 (12ms-20ms) (10) (unknown: 1) """ Best regards, david -------------- next part -------------- void testVariant(unsigned long n) { unsigned long i; i = n; /*@loop variant i; */ while (i >= 2UL) { i >>= 2UL; } } void testVariant_div(unsigned long n) { unsigned long i; i = n; /*@loop variant i; */ while (i >= 2UL) { i /= 4UL; } }