Relational-Spec/Loc.v at master · lyonel2017/Relational-Spec · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
From Stdlib Require Import Arith.

(** Locations are natural numbers **)

Module Loc := Nat.

(** Defining a few Location names **)

Definition EAX : Loc.t:= 1.
Definition EBX : Loc.t:= 2.
Definition ECX : Loc.t:= 3.
Definition EDX : Loc.t:= 4.
Definition EEX : Loc.t:= 5.
Definition EFX : Loc.t:= 6.
Definition EGX : Loc.t:= 7.
Definition EHX : Loc.t:= 8.

Definition X1 : Loc.t:= 1.
Definition X2 : Loc.t:= 2.
Definition X3 : Loc.t:= 3.
Definition ret : Loc.t := 3.
Definition X4 : Loc.t:= 4.

Definition a : Loc.t:= 1.
Definition b : Loc.t:= 2.
Definition x : Loc.t := 4.
Definition y : Loc.t:= 5.
Definition l : Loc.t:= 6.
Definition r : Loc.t:= 7.