Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (1.23 KB)

1
(* ---------------------------------------------------------- *)
2
(* --- Instance of 'Pre-condition (file oversampling0_4.c, line 138) in 'f_reset'' in 'g_reset' at call 'f_reset' (file oversampling0_4.c, line 321)
3
 --- *)
4
(* ---------------------------------------------------------- *)
5
Require Import ZArith.
6
Require Import Reals.
7
Require Import BuiltIn.
8
Require Import bool.Bool.
9
Require Import int.Int.
10
Require Import int.Abs.
11
Require Import int.ComputerDivision.
12
Require Import real.Real.
13
Require Import real.RealInfix.
14
Require Import real.FromInt.
15
Require Import map.Map.
16
Require Import Qedlib.
17
Require Import Qed.
18
Require Import Memory.
19

    
20
Require Import Axiomatic.
21
Require Import Compound.
22

    
23
Goal
24
  forall (t : array Z),
25
  forall (t_1 : farray addr addr),
26
  forall (a : addr),
27
  let a_1 := t_1.[ (shiftfield_F_g_mem_ni_1 a) ] in
28
  let a_2 := t_1.[ (shiftfield_F_g_mem_ni_0 a) ] in
29
  let a_3 := t_1.[ (shiftfield_F_f_mem_ni_2 a_2) ] in
30
  ((framed t_1)) ->
31
  ((linked t)) ->
32
  ((P_valid_g t t_1 a)) ->
33
  ((((region ((base a))%Z)) <= 0)%Z) ->
34
  (a_1 <> a_3) ->
35
  ((separated a 3%Z a_2 2%Z)) ->
36
  ((separated a 3%Z a_1 1%Z)) ->
37
  ((separated a_2 2%Z a_1 1%Z)) ->
38
  ((separated a 3%Z a_3 1%Z)) ->
39
  ((separated a_2 2%Z a_3 1%Z)) ->
40
  ((P_valid_f t t_1 a_2)).
41