--- layout: fc_discuss_archives title: Message 93 from Frama-C-discuss on November 2013 ---
Hi, CEA have done some works in WP to deals with ACSL bitwise operator: - internal simplification during WP calculus, - axiomatic for Alt-Ergo (to be extracted soon from a why3 axiomatic and proofs with Coq of the lemmas given to the external provers). There is a "good" specification of your rotate example for WP and also for the developer for my point of view: #define BIT_TEST(x,n) (((x)&(1<<(n)))!=0) /*@ ensures bit_zero: BIT_TEST(\result,0) <==> BIT_TEST(x,31); @ ensures other_bits: \forall integer k ; 0 <= k && k < 31 ==> ( BIT_TEST(\result,1+k) <==> BIT_TEST(x,k) ); */ unsigned rotate_left (unsigned x) { return (x << 1) | (x >> 31); } Once you guess what means this BIT_TEST macro inside an ACSL annotation, this specification become easy to understand: the bitwise operators (here: &, <<) apply to any mathematical integer (infinite 2-complement binary representation) (see page 22 of ASCL manual). The macro BIT_TEST(x,n) allow to specify the n-th bit (n=0 for the first bit) of x (and nothing is specified for negative value of n). Unfortunately, only parts of this work is inside Fluorine. With the development version, these two properties are proved, the first one by the internal simplifier Qed, the second one needs an external prover as Alt-Ergo: > frama-c -pp-annot rotate.c -wp [kernel] preprocessing with "gcc -C -E -I. -dD rotate.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] 2 goals scheduled [wp] [Qed] Goal typed_rotate_left_post_bit_zero : Valid (10ms) [wp] [Alt-Ergo] Goal typed_rotate_left_post_other_bits : Valid (2.6s) (1193) [wp] Proved goals: 2 / 2 Qed: 1 (10ms-10ms) Alt-Ergo: 1 (2.6s-2.6s) (1193) -- Patrick Le 12/11/2013 01:17, Claude Marche a ?crit : > Hi, > > The main reason is that the support of bitwise operators in Jessie in > very shallow, if any. > > I'm surprised that the first function could be proved. > > To succeed in proving such kind of code with Jessie, you should probably > provide properties on bitwise operators, under the form of lemmas. > > I'm not sure Jessie is the right tool for that, The Value plugin or the > WP plugin might do better. > > - Claude >