-
Notifications
You must be signed in to change notification settings - Fork 1
/
rec_granule_measure.v
66 lines (62 loc) · 2.54 KB
/
rec_granule_measure.v
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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
Require Import CodeDeps.
Require Import Ident.
Local Open Scope Z_scope.
Definition _data_size := 1%positive.
Definition _g := 2%positive.
Definition _granule := 3%positive.
Definition _rd := 4%positive.
Definition _rd__1 := 5%positive.
Definition _rec := 6%positive.
Definition _rec__1 := 7%positive.
Definition _reg := 8%positive.
Definition _ret := 9%positive.
Definition _size := 10%positive.
Definition rec_granule_measure_body :=
(Ssequence
(Scall None
(Evar _measurement_extend_rec_header (Tfunction
(Tcons (tptr Tvoid)
(Tcons
(tptr Tvoid)
Tnil)) tvoid cc_default))
((Etempvar _rd (tptr Tvoid)) ::
(Etempvar _rec (tptr Tvoid)) :: nil))
(Ssequence
(Scall None
(Evar _measurement_extend_rec_regs (Tfunction
(Tcons (tptr Tvoid)
(Tcons
(tptr Tvoid)
Tnil)) tvoid cc_default))
((Etempvar _rd (tptr Tvoid)) ::
(Etempvar _rec (tptr Tvoid)) :: nil))
(Ssequence
(Scall None
(Evar _measurement_extend_rec_pstate (Tfunction
(Tcons
(tptr Tvoid)
(Tcons
(tptr Tvoid)
Tnil)) tvoid cc_default))
((Etempvar _rd (tptr Tvoid)) ::
(Etempvar _rec (tptr Tvoid)) :: nil))
(Scall None
(Evar _measurement_extend_rec_sysregs (Tfunction
(Tcons
(tptr Tvoid)
(Tcons
(tptr Tvoid)
Tnil)) tvoid cc_default))
((Etempvar _rd (tptr Tvoid)) ::
(Etempvar _rec (tptr Tvoid)) :: nil)))))
.
Definition f_rec_granule_measure := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_rd, (tptr Tvoid)) ::
(_rec, (tptr Tvoid)) ::
(_data_size, tulong) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := rec_granule_measure_body
|}.