Commit 8e7a73c2 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Add cast in the definition of rc_copy_alloc_id.

parent 3d8fceab
Pipeline #47249 passed with stage
in 33 minutes and 33 seconds
......@@ -97,12 +97,12 @@ Section code.
Definition loc_124 : location_info := LocationInfo file_0 89 28 89 29.
Definition loc_129 : location_info := LocationInfo file_0 99 2 99 30.
Definition loc_130 : location_info := LocationInfo file_0 100 2 100 27.
Definition loc_131 : location_info := LocationInfo file_0 101 2 101 52.
Definition loc_132 : location_info := LocationInfo file_0 101 9 101 51.
Definition loc_131 : location_info := LocationInfo file_0 101 2 101 71.
Definition loc_132 : location_info := LocationInfo file_0 101 9 101 70.
Definition loc_133 : location_info := LocationInfo file_0 101 35 101 38.
Definition loc_134 : location_info := LocationInfo file_0 101 35 101 38.
Definition loc_135 : location_info := LocationInfo file_0 101 47 101 50.
Definition loc_136 : location_info := LocationInfo file_0 101 47 101 50.
Definition loc_135 : location_info := LocationInfo file_0 101 40 101 43.
Definition loc_136 : location_info := LocationInfo file_0 101 40 101 43.
Definition loc_137 : location_info := LocationInfo file_0 100 11 100 26.
Definition loc_138 : location_info := LocationInfo file_0 100 19 100 26.
Definition loc_139 : location_info := LocationInfo file_0 100 20 100 21.
......@@ -129,7 +129,7 @@ Section code.
Definition loc_170 : location_info := LocationInfo file_0 110 28 110 29.
Definition loc_175 : location_info := LocationInfo file_0 122 2 122 30.
Definition loc_176 : location_info := LocationInfo file_0 123 2 123 26.
Definition loc_177 : location_info := LocationInfo file_0 124 2 124 49.
Definition loc_177 : location_info := LocationInfo file_0 124 2 124 68.
Definition loc_178 : location_info := LocationInfo file_0 125 2 125 13.
Definition loc_179 : location_info := LocationInfo file_0 126 2 126 11.
Definition loc_180 : location_info := LocationInfo file_0 126 9 126 10.
......@@ -139,11 +139,11 @@ Section code.
Definition loc_184 : location_info := LocationInfo file_0 125 11 125 12.
Definition loc_185 : location_info := LocationInfo file_0 125 11 125 12.
Definition loc_188 : location_info := LocationInfo file_0 124 2 124 3.
Definition loc_189 : location_info := LocationInfo file_0 124 6 124 48.
Definition loc_189 : location_info := LocationInfo file_0 124 6 124 67.
Definition loc_190 : location_info := LocationInfo file_0 124 32 124 35.
Definition loc_191 : location_info := LocationInfo file_0 124 32 124 35.
Definition loc_192 : location_info := LocationInfo file_0 124 44 124 47.
Definition loc_193 : location_info := LocationInfo file_0 124 44 124 47.
Definition loc_192 : location_info := LocationInfo file_0 124 37 124 40.
Definition loc_193 : location_info := LocationInfo file_0 124 37 124 40.
Definition loc_194 : location_info := LocationInfo file_0 123 11 123 25.
Definition loc_195 : location_info := LocationInfo file_0 123 18 123 25.
Definition loc_196 : location_info := LocationInfo file_0 123 19 123 20.
......@@ -153,33 +153,33 @@ Section code.
Definition loc_202 : location_info := LocationInfo file_0 122 28 122 29.
Definition loc_203 : location_info := LocationInfo file_0 122 28 122 29.
Definition loc_208 : location_info := LocationInfo file_0 135 2 135 30.
Definition loc_209 : location_info := LocationInfo file_0 136 2 136 80.
Definition loc_209 : location_info := LocationInfo file_0 136 2 136 99.
Definition loc_210 : location_info := LocationInfo file_0 137 2 137 12.
Definition loc_211 : location_info := LocationInfo file_0 137 9 137 11.
Definition loc_212 : location_info := LocationInfo file_0 137 9 137 11.
Definition loc_213 : location_info := LocationInfo file_0 137 10 137 11.
Definition loc_214 : location_info := LocationInfo file_0 137 10 137 11.
Definition loc_215 : location_info := LocationInfo file_0 136 11 136 79.
Definition loc_215 : location_info := LocationInfo file_0 136 11 136 98.
Definition loc_216 : location_info := LocationInfo file_0 136 37 136 40.
Definition loc_217 : location_info := LocationInfo file_0 136 37 136 40.
Definition loc_218 : location_info := LocationInfo file_0 136 62 136 78.
Definition loc_219 : location_info := LocationInfo file_0 136 70 136 77.
Definition loc_220 : location_info := LocationInfo file_0 136 71 136 72.
Definition loc_221 : location_info := LocationInfo file_0 136 71 136 72.
Definition loc_222 : location_info := LocationInfo file_0 136 75 136 76.
Definition loc_218 : location_info := LocationInfo file_0 136 42 136 58.
Definition loc_219 : location_info := LocationInfo file_0 136 50 136 57.
Definition loc_220 : location_info := LocationInfo file_0 136 51 136 52.
Definition loc_221 : location_info := LocationInfo file_0 136 51 136 52.
Definition loc_222 : location_info := LocationInfo file_0 136 55 136 56.
Definition loc_225 : location_info := LocationInfo file_0 135 16 135 29.
Definition loc_226 : location_info := LocationInfo file_0 135 28 135 29.
Definition loc_227 : location_info := LocationInfo file_0 135 28 135 29.
Definition loc_232 : location_info := LocationInfo file_0 146 2 146 30.
Definition loc_233 : location_info := LocationInfo file_0 147 2 147 26.
Definition loc_234 : location_info := LocationInfo file_0 148 2 148 55.
Definition loc_235 : location_info := LocationInfo file_0 148 9 148 54.
Definition loc_236 : location_info := LocationInfo file_0 148 9 148 54.
Definition loc_237 : location_info := LocationInfo file_0 148 10 148 54.
Definition loc_234 : location_info := LocationInfo file_0 148 2 148 74.
Definition loc_235 : location_info := LocationInfo file_0 148 9 148 73.
Definition loc_236 : location_info := LocationInfo file_0 148 9 148 73.
Definition loc_237 : location_info := LocationInfo file_0 148 10 148 73.
Definition loc_238 : location_info := LocationInfo file_0 148 37 148 40.
Definition loc_239 : location_info := LocationInfo file_0 148 37 148 40.
Definition loc_240 : location_info := LocationInfo file_0 148 49 148 52.
Definition loc_241 : location_info := LocationInfo file_0 148 49 148 52.
Definition loc_240 : location_info := LocationInfo file_0 148 42 148 45.
Definition loc_241 : location_info := LocationInfo file_0 148 42 148 45.
Definition loc_242 : location_info := LocationInfo file_0 147 11 147 25.
Definition loc_243 : location_info := LocationInfo file_0 147 18 147 25.
Definition loc_244 : location_info := LocationInfo file_0 147 19 147 20.
......@@ -189,12 +189,12 @@ Section code.
Definition loc_250 : location_info := LocationInfo file_0 146 28 146 29.
Definition loc_251 : location_info := LocationInfo file_0 146 28 146 29.
Definition loc_256 : location_info := LocationInfo file_0 156 2 156 28.
Definition loc_257 : location_info := LocationInfo file_0 157 2 157 54.
Definition loc_258 : location_info := LocationInfo file_0 157 9 157 53.
Definition loc_257 : location_info := LocationInfo file_0 157 2 157 73.
Definition loc_258 : location_info := LocationInfo file_0 157 9 157 72.
Definition loc_259 : location_info := LocationInfo file_0 157 36 157 39.
Definition loc_260 : location_info := LocationInfo file_0 157 36 157 39.
Definition loc_261 : location_info := LocationInfo file_0 157 48 157 51.
Definition loc_262 : location_info := LocationInfo file_0 157 48 157 51.
Definition loc_261 : location_info := LocationInfo file_0 157 41 157 44.
Definition loc_262 : location_info := LocationInfo file_0 157 41 157 44.
Definition loc_263 : location_info := LocationInfo file_0 156 12 156 27.
Definition loc_264 : location_info := LocationInfo file_0 156 20 156 27.
Definition loc_265 : location_info := LocationInfo file_0 156 21 156 22.
......
......@@ -522,10 +522,10 @@ let rec translate_expr : bool -> op_type option -> ail_expr -> expr =
| _ -> not_impl loc "wrong macro"
end
| AilEcond(e1,e2,e3) when is_const_0 e1 && is_copy_alloc_id_annot e2 ->
let e2 =
let (e2, e3) =
match macro_annot_to_list e2 with
| [_; MacroExpr(e2); _] -> e2
| _ ->
| [_; MacroExpr(e2); MacroExpr(e3)] -> (e2, e3)
| _ ->
not_impl loc "wrong copy alloc id annotation"
in
let ot2 = op_type_of_tc (loc_of e2) (tc_of e2) in
......
......@@ -39,6 +39,9 @@
#define RC_MACRO_EXPR(expr) "EXPR", expr
#define RC_MACRO(name, m, ...) (0 ? ("rc_macro", #name, __VA_ARGS__, (m)) : (m))
#define rc_copy_alloc_id(to, from) (0 ? ("rc_copy_alloc_id", (from), (to)) : (to))
// Note that rc_copy_alloc_id exposes the provenance of [from] by casting it
// to an integer (throwing away the result).
#define rc_copy_alloc_id(to, from) \
(0 ? ("rc_copy_alloc_id", (from), (to)) : ((uintptr_t) (from), (to)))
#endif
......@@ -26,31 +26,31 @@ Section code.
Definition loc_21 : location_info := LocationInfo file_0 80 2 84 3.
Definition loc_22 : location_info := LocationInfo file_0 80 7 80 12.
Definition loc_23 : location_info := LocationInfo file_0 80 2 84 3.
Definition loc_24 : location_info := LocationInfo file_0 86 2 86 83.
Definition loc_25 : location_info := LocationInfo file_0 86 9 86 82.
Definition loc_24 : location_info := LocationInfo file_0 86 2 86 111.
Definition loc_25 : location_info := LocationInfo file_0 86 9 86 110.
Definition loc_26 : location_info := LocationInfo file_0 86 35 86 47.
Definition loc_27 : location_info := LocationInfo file_0 86 35 86 47.
Definition loc_28 : location_info := LocationInfo file_0 86 37 86 40.
Definition loc_29 : location_info := LocationInfo file_0 86 67 86 81.
Definition loc_30 : location_info := LocationInfo file_0 86 77 86 80.
Definition loc_31 : location_info := LocationInfo file_0 86 77 86 80.
Definition loc_29 : location_info := LocationInfo file_0 86 49 86 63.
Definition loc_30 : location_info := LocationInfo file_0 86 59 86 62.
Definition loc_31 : location_info := LocationInfo file_0 86 59 86 62.
Definition loc_32 : location_info := LocationInfo file_0 80 33 84 3.
Definition loc_33 : location_info := LocationInfo file_0 81 4 81 18.
Definition loc_34 : location_info := LocationInfo file_0 81 18 81 5.
Definition loc_35 : location_info := LocationInfo file_0 82 4 82 24.
Definition loc_36 : location_info := LocationInfo file_0 83 4 83 88.
Definition loc_36 : location_info := LocationInfo file_0 83 4 83 116.
Definition loc_37 : location_info := LocationInfo file_0 80 2 84 3.
Definition loc_38 : location_info := LocationInfo file_0 80 28 80 31.
Definition loc_39 : location_info := LocationInfo file_0 80 28 80 29.
Definition loc_40 : location_info := LocationInfo file_0 83 4 83 14.
Definition loc_41 : location_info := LocationInfo file_0 83 4 83 14.
Definition loc_42 : location_info := LocationInfo file_0 83 15 83 86.
Definition loc_42 : location_info := LocationInfo file_0 83 15 83 114.
Definition loc_43 : location_info := LocationInfo file_0 83 41 83 53.
Definition loc_44 : location_info := LocationInfo file_0 83 41 83 53.
Definition loc_45 : location_info := LocationInfo file_0 83 43 83 46.
Definition loc_46 : location_info := LocationInfo file_0 83 72 83 85.
Definition loc_47 : location_info := LocationInfo file_0 83 81 83 84.
Definition loc_48 : location_info := LocationInfo file_0 83 81 83 84.
Definition loc_46 : location_info := LocationInfo file_0 83 55 83 68.
Definition loc_47 : location_info := LocationInfo file_0 83 64 83 67.
Definition loc_48 : location_info := LocationInfo file_0 83 64 83 67.
Definition loc_49 : location_info := LocationInfo file_0 82 4 82 5.
Definition loc_50 : location_info := LocationInfo file_0 82 8 82 23.
Definition loc_51 : location_info := LocationInfo file_0 82 8 82 11.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment