Commit 5a0032f2 authored by François Bobot's avatar François Bobot

list_rev.mlw : just a trivial check needed for automatic generation

parent 01d6d03f
......@@ -203,6 +203,10 @@ module M2
forall next : next, p : pointer.
p <> null -> is_list next (get next p) -> is_list next p
goal is_list_disjoint_case :
forall next : next, p : pointer.
p = null /\ p <> null /\ is_list next (get next p) -> false
(** Frame for is_list *)
type ft 'a
......@@ -18,6 +18,11 @@
<theory name="M2" verified="false" expanded="true">
<goal name="is_list_disjoint_case" sum="1babcc38937f94867ddd31ce304b7e74" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<goal name="frame_list" sum="6832b0f09ea49b1a68df28ae5d8cc5ba" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="list_rev.mlw_M2_frame_list_1.v" obsolete="false">
<result status="valid" time="0.72"/>
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment