Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP and memcpy question

  • Subject: [Frama-c-discuss] WP and memcpy question
  • From: agoodloe at gmail.com (Alwyn Goodloe)
  • Date: Mon, 18 Jun 2018 18:44:48 -0400
The annotated C file below The last function  is given as follows

/*@ requires 0 <= s0_idx < 1;
    requires 0 <= s1_idx < 2;
    requires  \separated(exarr_cpy + (0..2), exarr + (0..2));
    requires \separated(s1, exarr_cpy+(0..2));
    requires \separated(s1, exarr+(0..2));
    requires \separated(&s0, exarr_cpy+(0..2));
    requires \separated(&s0, exarr+(0..2));
    assigns  s0;
    assigns  s1;
    assigns  s0_buff[s0_idx];
    assigns  s1_buff[s1_idx][0];
    assigns  s1_buff[s1_idx][1];
    assigns  s1_buff[s1_idx][2];
    assigns  s0_idx;
    assigns  s1_idx;
    ensures  0 <= s0_idx < 1;
    ensures  0 <= s1_idx < 2;
    ensures  \forall int i; 0 <= i < 1&& i != \old(s0_idx) ==>
        s0_buff[i] == \old(s0_buff[i]);
    ensures  \forall int i; 0 <= i < 2&& i != \old(s1_idx) ==>
        s1_buff[i] == \old(s1_buff[i]);
*/
static void step () {
  memcpy(exarr_cpy, exarr, sizeof(exarr_cpy));
  if (farray_guard()) {farray(farray_arg0(),
                       farray_arg1(),
                       farray_arg2());
                     }
  s0 = s0_gen();
  s1 = s1_gen();
  int8_t s1_tmp[3];
  memcpy(s1_tmp, s1, sizeof(s1_tmp));
  /*@ assert 0 <= s0_idx < 1; */
  s0_buff[s0_idx] = s0;
  memcpy(s1_buff[s1_idx], s1_tmp, sizeof(s1_tmp));
  ++(s0_idx);
  ++(s1_idx);
  s0_idx = s0_idx % 1;
  s1_idx = s1_idx % 2;
}


When I run wp with both alt-ergo and Z3 provers all but four VCs are
discharged Each unproven VC seems related to memcpy and the goal is always
the assigns s0 in line 117.  Any suggestions on what I might need to do in
order to would be appreciated.  Here is one of messages  produced for one
of the unproved VCs.

Goal Assigns (file NewArray.c, line 117) in 'step' (2/14):
Call Effect at line 133
Assume {
  Type: is_uint32(s0_idx_0) /\ is_uint32(s1_idx_0) /\ is_sint32(status_0).
  (* Heap *)
  Have: (region(s1_0.base) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0).
  (* Pre-condition *)
  Have: (s0_idx_0 <= 0) /\ (0 <= s0_idx_0).
  (* Pre-condition *)
  Have: (0 <= s1_idx_0) /\ (s1_idx_0 <= 1).
  (* Pre-condition *)
  Have: separated(s1_0, 1, shift_sint8(global(G_exarr_cpy_1569), 0), 3).
  (* Pre-condition *)
  Have: separated(s1_0, 1, shift_sint8(global(G_exarr_1191), 0), 3).
  (* Merge *)
  Either {
    Case:
      Let a = shift_sint8(global(G_exarr_cpy_1569), 0).
      (* Call 'memcpy' *)
      Have: L_memcmp(Mchar_0, Mchar_1, a,
              shift_sint8(global(G_exarr_1191), 0), 3) = 0.
      (* Call Effects *)
      Have: havoc(Mchar_0, Mchar_1, a, 3).
    Case: (* Exit Effects *) Have: havoc(Mchar_0, Mchar_2, a, 3).
  }
}
Prove: false.
Prover Z3 returns Failed
Why3 exits with status 1.
Prover Alt-Ergo returns Unknown (Qed:5ms) (271ms)



-- 
Alwyn E. Goodloe, Ph.D.
agoodloe at gmail.com

Research Computer Engineer
NASA Langley Research Center
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180618/19be869c/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: NewArray.c
Type: application/octet-stream
Size: 3319 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180618/19be869c/attachment.obj>