--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on June 2018 ---
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>