|
1
|
(* ---------------------------------------------------------- *)
|
|
2
|
(* --- Struct 'g_reg' --- *)
|
|
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
|
|
|
19
|
Record S_g_reg : Type := { F_g_reg___g_2 : Z }.
|
|
20
|
Require Import Cint.
|
|
21
|
|
|
22
|
Definition IsS_g_reg (S : S_g_reg) : Prop := (is_sint32 (F_g_reg___g_2 S)%Z).
|
|
23
|
|