Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / clocks7 / wp1.script @ 6a93d814

History | View | Annotate | Download (737 Bytes)

1
(* Generated by Frama-C WP *)
2

    
3
Goal typed_toto_step_assert_6.
4
Hint property,toto_step.
5
Proof.
6
intros.
7
unfold P_trans_totoH.
8
intuition.
9
unfold P_trans_totoG.
10
exists Z0.
11
exists Z0.
12
exists Z0.
13
intuition.
14
unfold is_sint32.
15
auto with zarith.
16
unfold is_sint32.
17
auto with zarith.
18
unfold is_uint32.
19
auto with zarith.
20
unfold P_trans_totoF.
21
unfold P_trans_totoE.
22
unfold P_trans_totoD.
23
intuition.
24
exists Z0.
25
unfold is_uint32.
26
intuition.
27

    
28
unfold P_trans_totoC.
29
unfold P_trans_totoB.
30
unfold P_clock_toto_2.
31
intuition.
32
discriminate.
33
unfold P_clock_c in H7.
34
discriminate.
35
unfold P_clock_b2 in H7.
36
intuition.
37
unfold P_clock_c in H10.
38
discriminate.
39
unfold P_clock_b1 in H7.
40
intuition.
41
unfold P_clock_z in H7.
42
unfold P_clock_c in H7.
43
discriminate.
44
Qed.
45

    
46