generated_code.v 5.2 KB
Newer Older
1
2
3
4
5
6
7
From refinedc.lang Require Export notation.
From refinedc.lang Require Import tactics.
From refinedc.typing Require Import annotations.
Set Default Proof Using "Type".

(* Generated from [tutorial/t10_loops.c]. *)
Section code.
8
  Definition file_0 : string := "include/refinedc.h".
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
  Definition file_1 : string := "tutorial/t10_loops.c".
  Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
  Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.
  Definition loc_4 : location_info := LocationInfo file_0 49 9 49 32.
  Definition loc_5 : location_info := LocationInfo file_0 49 33 49 37.
  Definition loc_6 : location_info := LocationInfo file_0 49 33 49 37.
  Definition loc_7 : location_info := LocationInfo file_0 49 39 49 45.
  Definition loc_8 : location_info := LocationInfo file_0 49 39 49 45.
  Definition loc_11 : location_info := LocationInfo file_1 7 2 7 18.
  Definition loc_12 : location_info := LocationInfo file_1 10 2 10 18.
  Definition loc_13 : location_info := LocationInfo file_1 13 2 13 18.
  Definition loc_14 : location_info := LocationInfo file_1 13 2 13 18.
  Definition loc_15 : location_info := LocationInfo file_1 13 16 13 18.
  Definition loc_16 : location_info := LocationInfo file_1 13 2 13 18.
  Definition loc_17 : location_info := LocationInfo file_1 13 2 13 18.
  Definition loc_18 : location_info := LocationInfo file_1 13 8 13 14.
  Definition loc_19 : location_info := LocationInfo file_1 13 8 13 9.
  Definition loc_20 : location_info := LocationInfo file_1 13 8 13 9.
  Definition loc_21 : location_info := LocationInfo file_1 13 13 13 14.
  Definition loc_22 : location_info := LocationInfo file_1 10 2 10 18.
  Definition loc_23 : location_info := LocationInfo file_1 10 16 10 18.
  Definition loc_24 : location_info := LocationInfo file_1 10 2 10 18.
  Definition loc_25 : location_info := LocationInfo file_1 10 2 10 18.
  Definition loc_26 : location_info := LocationInfo file_1 10 8 10 14.
  Definition loc_27 : location_info := LocationInfo file_1 10 8 10 9.
  Definition loc_28 : location_info := LocationInfo file_1 10 8 10 9.
  Definition loc_29 : location_info := LocationInfo file_1 10 13 10 14.
  Definition loc_30 : location_info := LocationInfo file_1 7 2 7 18.
  Definition loc_31 : location_info := LocationInfo file_1 7 16 7 18.
  Definition loc_32 : location_info := LocationInfo file_1 7 2 7 18.
  Definition loc_33 : location_info := LocationInfo file_1 7 2 7 18.
  Definition loc_34 : location_info := LocationInfo file_1 7 8 7 14.
  Definition loc_35 : location_info := LocationInfo file_1 7 8 7 9.
  Definition loc_36 : location_info := LocationInfo file_1 7 8 7 9.
  Definition loc_37 : location_info := LocationInfo file_1 7 13 7 14.

  (* Definition of function [copy_alloc_id]. *)
  Definition impl_copy_alloc_id : function := {|
    f_args := [
      ("to", it_layout uintptr_t);
      ("from", void*)
    ];
    f_local_vars := [
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
        locinfo: loc_2 ;
Michael Sammler's avatar
Michael Sammler committed
57
        Return (LocInfoE loc_3 (CopyAllocId (IntOp uintptr_t) (LocInfoE loc_5 (use{IntOp uintptr_t} (LocInfoE loc_6 ("to")))) (LocInfoE loc_7 (use{PtrOp} (LocInfoE loc_8 ("from"))))))
58
59
60
      ]> $
    )%E
  |}.
61
62
63
64
65
66
67
68
69
70
71

  (* Definition of function [loop_without_annot]. *)
  Definition impl_loop_without_annot : function := {|
    f_args := [
      ("a", it_layout i32)
    ];
    f_local_vars := [
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
72
        locinfo: loc_11 ;
73
74
75
        Goto "#1"
      ]> $
      <[ "#1" :=
76
        locinfo: loc_34 ;
Michael Sammler's avatar
Michael Sammler committed
77
        if: LocInfoE loc_34 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_34 ((LocInfoE loc_35 (use{IntOp i32} (LocInfoE loc_36 ("a")))) ={IntOp i32, IntOp i32} (LocInfoE loc_37 (i2v 1 i32)))))
78
        then
79
        locinfo: loc_32 ;
80
81
          Goto "#2"
        else
82
        locinfo: loc_12 ;
83
84
85
          Goto "#3"
      ]> $
      <[ "#2" :=
86
87
        locinfo: loc_32 ;
        Goto "continue4"
88
89
      ]> $
      <[ "#3" :=
90
        locinfo: loc_12 ;
91
92
93
        Goto "#4"
      ]> $
      <[ "#4" :=
94
        locinfo: loc_26 ;
Michael Sammler's avatar
Michael Sammler committed
95
        if: LocInfoE loc_26 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_26 ((LocInfoE loc_27 (use{IntOp i32} (LocInfoE loc_28 ("a")))) ={IntOp i32, IntOp i32} (LocInfoE loc_29 (i2v 1 i32)))))
96
        then
97
        locinfo: loc_24 ;
98
99
          Goto "#5"
        else
100
        locinfo: loc_13 ;
101
102
103
          Goto "#6"
      ]> $
      <[ "#5" :=
104
105
        locinfo: loc_24 ;
        Goto "continue6"
106
107
      ]> $
      <[ "#6" :=
108
        locinfo: loc_13 ;
109
110
111
        Goto "#7"
      ]> $
      <[ "#7" :=
112
        locinfo: loc_18 ;
Michael Sammler's avatar
Michael Sammler committed
113
        if: LocInfoE loc_18 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_18 ((LocInfoE loc_19 (use{IntOp i32} (LocInfoE loc_20 ("a")))) ={IntOp i32, IntOp i32} (LocInfoE loc_21 (i2v 1 i32)))))
114
        then
115
        locinfo: loc_16 ;
116
117
118
119
120
          Goto "#8"
        else
        Goto "#9"
      ]> $
      <[ "#8" :=
121
122
        locinfo: loc_16 ;
        Goto "continue8"
123
124
125
126
      ]> $
      <[ "#9" :=
        Return (VOID)
      ]> $
127
128
      <[ "continue4" :=
        locinfo: loc_11 ;
129
130
        Goto "#1"
      ]> $
131
132
      <[ "continue6" :=
        locinfo: loc_12 ;
133
134
        Goto "#4"
      ]> $
135
136
      <[ "continue8" :=
        locinfo: loc_13 ;
137
138
139
140
141
        Goto "#7"
      ]> $
    )%E
  |}.
End code.