97 open Hints_declaration
107 (** val is_cost_label : RTLabs_syntax.statement -> Bool.bool **)
108 let is_cost_label = function
109 | RTLabs_syntax.St_skip x -> Bool.False
110 | RTLabs_syntax.St_cost (x, x0) -> Bool.True
111 | RTLabs_syntax.St_const (x, x0, x1, x2) -> Bool.False
112 | RTLabs_syntax.St_op1 (x, x0, x1, x2, x3, x4) -> Bool.False
113 | RTLabs_syntax.St_op2 (x, x0, x1, x2, x3, x4, x5, x6) -> Bool.False
114 | RTLabs_syntax.St_load (x, x0, x1, x2) -> Bool.False
115 | RTLabs_syntax.St_store (x, x0, x1, x2) -> Bool.False
116 | RTLabs_syntax.St_call_id (x, x0, x1, x2) -> Bool.False
117 | RTLabs_syntax.St_call_ptr (x, x0, x1, x2) -> Bool.False
118 | RTLabs_syntax.St_cond (x, x0, x1) -> Bool.False
119 | RTLabs_syntax.St_return -> Bool.False
121 (** val cost_label_of :
122 RTLabs_syntax.statement -> CostLabel.costlabel Types.option **)
123 let cost_label_of = function
124 | RTLabs_syntax.St_skip x -> Types.None
125 | RTLabs_syntax.St_cost (s0, x) -> Types.Some s0
126 | RTLabs_syntax.St_const (x, x0, x1, x2) -> Types.None
127 | RTLabs_syntax.St_op1 (x, x0, x1, x2, x3, x4) -> Types.None
128 | RTLabs_syntax.St_op2 (x, x0, x1, x2, x3, x4, x5, x6) -> Types.None
129 | RTLabs_syntax.St_load (x, x0, x1, x2) -> Types.None
130 | RTLabs_syntax.St_store (x, x0, x1, x2) -> Types.None
131 | RTLabs_syntax.St_call_id (x, x0, x1, x2) -> Types.None
132 | RTLabs_syntax.St_call_ptr (x, x0, x1, x2) -> Types.None
133 | RTLabs_syntax.St_cond (x, x0, x1) -> Types.None
134 | RTLabs_syntax.St_return -> Types.None
136 (** val well_cost_labelled_statement :
137 RTLabs_syntax.statement Graphs.graph -> RTLabs_syntax.statement ->
139 let well_cost_labelled_statement g s =
141 | RTLabs_syntax.St_skip x -> (fun _ -> Bool.True)
142 | RTLabs_syntax.St_cost (x, x0) -> (fun _ -> Bool.True)
143 | RTLabs_syntax.St_const (x, x0, x1, x2) -> (fun _ -> Bool.True)
144 | RTLabs_syntax.St_op1 (x, x0, x1, x2, x3, x4) -> (fun _ -> Bool.True)
145 | RTLabs_syntax.St_op2 (x, x0, x1, x2, x3, x4, x5, x6) ->
147 | RTLabs_syntax.St_load (x, x0, x1, x2) -> (fun _ -> Bool.True)
148 | RTLabs_syntax.St_store (x, x0, x1, x2) -> (fun _ -> Bool.True)
149 | RTLabs_syntax.St_call_id (x, x0, x1, x2) -> (fun _ -> Bool.True)
150 | RTLabs_syntax.St_call_ptr (x, x0, x1, x2) -> (fun _ -> Bool.True)
151 | RTLabs_syntax.St_cond (x, l1, l2) ->
155 (Identifiers.lookup_present PreIdentifiers.LabelTag g l1))
157 (Identifiers.lookup_present PreIdentifiers.LabelTag g l2)))
158 | RTLabs_syntax.St_return -> (fun _ -> Bool.True)) __
160 (** val successors : RTLabs_syntax.statement -> Graphs.label List.list **)
161 let rec successors = function
162 | RTLabs_syntax.St_skip l -> List.Cons (l, List.Nil)
163 | RTLabs_syntax.St_cost (x, l) -> List.Cons (l, List.Nil)
164 | RTLabs_syntax.St_const (x, x0, x1, l) -> List.Cons (l, List.Nil)
165 | RTLabs_syntax.St_op1 (x, x0, x1, x2, x3, l) -> List.Cons (l, List.Nil)
166 | RTLabs_syntax.St_op2 (x, x0, x1, x2, x3, x4, x5, l) ->
167 List.Cons (l, List.Nil)
168 | RTLabs_syntax.St_load (x, x0, x1, l) -> List.Cons (l, List.Nil)
169 | RTLabs_syntax.St_store (x, x0, x1, l) -> List.Cons (l, List.Nil)
170 | RTLabs_syntax.St_call_id (x, x0, x1, l) -> List.Cons (l, List.Nil)
171 | RTLabs_syntax.St_call_ptr (x, x0, x1, l) -> List.Cons (l, List.Nil)
172 | RTLabs_syntax.St_cond (x, l1, l2) ->
173 List.Cons (l1, (List.Cons (l2, List.Nil)))
174 | RTLabs_syntax.St_return -> List.Nil