Search code examples
frama-c

Format of weakest precondition printed by wp plugin

I dont understand the format of wp printed by wp plugin in frama-c. An example:

Goal Assertion 'P402926' (file gzip-1.5/deflate.c, line 479):
Let x_0 = Mint_0[(shift match_8 1)].
Let x_1 = Mint_0[(shift scan_16 1)].
Let x_2 = Mint_0[(shift scan_17 1)].
Let a_0 = (global G_window_2513).
Let x_3 = Mint_0[(shift a_0 (1+cur_match_1))].
Let x_4 = Mint_0[scan_17].
Let x_5 = Mint_0[(shift a_0 cur_match_1)].
Assume {
  (* Domain *)
  Type: (is_sint32 best_len_1) /\ (is_sint32 len_0)
        /\ (is_uint32 cur_match_1) /\ (is_uint8 Mint_0[match_0])
        /\ (is_uint8 Mint_0[match_1]) /\ (is_uint8 Mint_0[match_2])
        /\ (is_uint8 Mint_0[match_3]) /\ (is_uint8 Mint_0[match_4])
        /\ (is_uint8 Mint_0[match_5]) /\ (is_uint8 Mint_0[match_6])
        /\ (is_uint8 Mint_0[scan_1]) /\ (is_uint8 Mint_0[scan_3])
        /\ (is_uint8 Mint_0[scan_5]) /\ (is_uint8 Mint_0[scan_7])
        /\ (is_uint8 Mint_0[scan_9]) /\ (is_uint8 Mint_0[scan_11])
        /\ (is_uint8 Mint_0[scan_13]) /\ (is_uint8 x_4) /\ (is_uint8 x_0)
        /\ (is_uint8 x_1) /\ (is_uint8 x_2) /\ (is_uint8 x_5)
        /\ (is_uint16
(* gzip-1.5/deflate.c:453: Else *)
  Have: x_4=x_5.
  (* gzip-1.5/deflate.c:454: Else *)
  Have: x_2=x_3.
  (* gzip-1.5/deflate.c:468: Conditional *)
  If: x_0=x_1
  Then {
    (* gzip-1.5/deflate.c:468: Conditional *)
    If: Mint_0[(shift match_8 2)]=Mint_0[(shift scan_16 2)]
    Then {
      (* gzip-1.5/deflate.c:469: Conditional *)
      If: Mint_0[(shift match_8 3)]=Mint_0[(shift scan_16 3)]
      Then { .....

Many extra variables have been introduced which i dont understand like shift, global,etc, which are not in the program..

Can some one explain?

Solution

  • You can find a brief description of the internal language used by WP for building proof obligations in chapters 3 and 4 of the WP manual. Additionally, the built-in functions and predicates that appear in the formula are defined in the various .why files in $(frama-c -print-share-path)/wp/why3, especially Memory.why which axiomatize all memory-related operations.

    To answer your main interrogations:

    1. if-else is here to avoid an exponential blow-up in the number of proof obligations with respect to the number of branches of each function (at the expense of a slightly more complicated formula)
    2. global takes the address of a global. You can see here that a0 is then used as an index in the Mint_0 map (which maps addresses of the form base + offset to values).
    3. shift moves the offset of an address: shift a_0 cur_match_1 refers to the corresponding cell of the window array.