Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (1.95 KB)

1 6a93d814 xthirioux
(* ---------------------------------------------------------- *)
2
(* --- Assertion (file oversampling0_4.c, line 342)       --- *)
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 Compound.
21
Require Import Axiomatic.
22
Require Import Cint.
23
24
Goal
25
  forall (t : array Z),
26
  forall (t_2 t_1 : farray addr Z),
27
  forall (t_3 : farray addr addr),
28
  forall (a_1 a : addr),
29
  forall (g_1 g : S_g_mem_pack),
30
  let a_2 := t_3.[ (shiftfield_F_g_mem_ni_1 a_1) ] in
31
  let a_3 := t_3.[ (shiftfield_F_g_mem_ni_0 a_1) ] in
32
  let a_4 := t_3.[ (shiftfield_F_f_mem_ni_2 a_3) ] in
33
  let a_5 := (shiftfield_F__arrow_reg__first
34
               ((shiftfield_F__arrow_mem__reg a_2))) in
35
  let x := (t_2.[ a_5 ])%Z in
36
  ((IsS_g_mem_pack g)) ->
37
  ((IsS_g_mem_pack g_1)) ->
38
  ((framed t_3)) ->
39
  ((linked t)) ->
40
  (a <> a_2) ->
41
  ((valid_rw t a 1%Z)) ->
42
  ((P_valid_g t t_3 a_1)) ->
43
  ((((region ((base a))%Z)) <= 0)%Z) ->
44
  ((((region ((base a_1))%Z)) <= 0)%Z) ->
45
  ((separated a_1 3%Z a 1%Z)) ->
46
  ((P_g_pack1 t_3 t_1 g a_1)) ->
47
  ((P_g_pack3 t_3 t_2 g_1 a_1)) ->
48
  (a <> a_4) ->
49
  (a_2 <> a_4) ->
50
  ((separated a 1%Z a_3 2%Z)) ->
51
  ((separated a_1 3%Z a_3 2%Z)) ->
52
  ((separated a_1 3%Z a_2 1%Z)) ->
53
  ((separated a_3 2%Z a_2 1%Z)) ->
54
  ((is_uint32 x)) ->
55
  ((separated a_1 3%Z a_4 1%Z)) ->
56
  ((separated a_3 2%Z a_4 1%Z)) ->
57
  (itep ((0 = x)%Z) (t_1 = t_2) (t_1 = (t_2.[ a_5 <- (0)%Z ]))) ->
58
  (forall (g_2 : S_g_mem_pack), ((IsS_g_mem_pack g_2)) ->
59
   (forall (g_3 : S_g_mem_pack), (P_g_pack0) -> ((IsS_g_mem_pack g_3)) ->
60
    ((P_g_pack3 t_3 t_2 g_2 a_1)) -> (P_trans_gA))) ->
61
  ((P_trans_gB g_1 g x)).