assigns clause appears unprovable
ID0001638: This issue was created automatically from Mantis Issue 1638. Further discussion may take place here.
|ID0001638||Frama-C||Plug-in > wp||public||2014-02-01||2014-07-17|
|Product Version||Frama-C Fluorine-20130601||Target Version||-||Fixed in Version||-|
It appears that assigns clauses of functions that modify an array cannot be verified at all. I attach a simple example of a function set_zero that sets all elements of an array to zero (file set_zero.c). Attached is also an attempt to prove the assigns clause with Coq (see file wp0.script). I do not see how from 0 <= n 0 < i one can conclude i <= n
Please, correct me if I am totally missing something.
Additional Information :
Here is my proof attempt for the assigns clause:
Proof. forward. remember a_0 as a. remember n_0 as n. remember i_0 as i. remember Mint_0 as M0. remember Mint_1 as M1.
cut (i <= n). auto with zarith.
assert(less_equal: 0 <= n). assumption. apply Zle_lt_or_eq in less_equal. rewrite or_comm in less_equal.
destruct less_equal as [equal | less]. (* case equal *) rewrite <- equal. assert (~(i <= 0)). auto with zarith. contradict H7.
(* what now ? *)