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

History | View | Annotate | Download (1.23 KB)

1 | 6a93d814 | xthirioux | (* ---------------------------------------------------------- *) |
---|---|---|---|

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)). |