Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / oversampling / out / typed / g_reset_post.coq @ 6a93d814

History | View | Annotate | Download (1.68 KB)

1
(* ---------------------------------------------------------- *)
2
(* --- Post-condition (file oversampling0_4.c, line 316) in 'g_reset' --- *)
3
(* ---------------------------------------------------------- *)
4
Require Import ZArith.
5
Require Import Reals.
6
Require Import BuiltIn.
7
Require Import bool.Bool.
8
Require Import int.Int.
9
Require Import int.Abs.
10
Require Import int.ComputerDivision.
11
Require Import real.Real.
12
Require Import real.RealInfix.
13
Require Import real.FromInt.
14
Require Import map.Map.
15
Require Import Qedlib.
16
Require Import Qed.
17

    
18
Require Import S_g_mem_pack.
19
Require Import Memory.
20
Require Import Axiomatic.
21
Require Import Compound.
22
Require Import S_f_mem_pack.
23

    
24
Goal
25
  forall (i : Z),
26
  forall (t : array Z),
27
  forall (t_1 : farray addr Z),
28
  forall (t_2 : farray addr addr),
29
  forall (a : addr),
30
  forall (g : S_g_mem_pack),
31
  let a_1 := t_2.[ (shiftfield_F_g_mem_ni_1 a) ] in
32
  let a_2 := t_2.[ (shiftfield_F_g_mem_ni_0 a) ] in
33
  let a_3 := t_2.[ (shiftfield_F_f_mem_ni_2 a_2) ] in
34
  let m := (t_1.[ (shiftfield_F__arrow_reg__first
35
                    ((shiftfield_F__arrow_mem__reg a_1))) <- (1)%Z ]).[ 
36
      (shiftfield_F__arrow_reg__first ((shiftfield_F__arrow_mem__reg a_3))) <- 
37
      (i)%Z ] in
38
  ((IsS_g_mem_pack g)) ->
39
  ((framed t_2)) ->
40
  ((linked t)) ->
41
  ((P_valid_g t t_2 a)) ->
42
  ((((region ((base a))%Z)) <= 0)%Z) ->
43
  (a_1 <> a_3) ->
44
  ((P_valid_f t t_2 a_2)) ->
45
  ((separated a 3%Z a_2 2%Z)) ->
46
  ((separated a 3%Z a_1 1%Z)) ->
47
  ((separated a_2 2%Z a_1 1%Z)) ->
48
  ((separated a 3%Z a_3 1%Z)) ->
49
  ((separated a_2 2%Z a_3 1%Z)) ->
50
  ((P_g_pack3 t_2 m g a)) ->
51
  (forall (f : S_f_mem_pack), ((IsS_f_mem_pack f)) ->
52
   ((P_f_pack2 t_2 m f a_2)) -> ((P_init_f f))) ->
53
  ((P_init_g g)).
54