Revision 25b4311f
src/machine_code.ml | ||
---|---|---|
280 | 280 |
in |
281 | 281 |
aux [] eqs |
282 | 282 |
|
283 |
(* specialize predefined (polymorphic) operators |
|
284 |
wrt their instances, so that the C semantics |
|
285 |
is preserved *) |
|
286 |
let specialize_to_c expr = |
|
287 |
match expr.expr_desc with |
|
288 |
| Expr_appl (id, e, r) -> |
|
289 |
if List.exists (fun e -> Types.is_bool_type e.expr_type) (expr_list_of_expr e) |
|
290 |
then let id = |
|
291 |
match id with |
|
292 |
| "=" -> "equi" |
|
293 |
| "!=" -> "xor" |
|
294 |
| _ -> id in |
|
295 |
{ expr with expr_desc = Expr_appl (id, e, r) } |
|
296 |
else expr |
|
297 |
| _ -> expr |
|
298 |
|
|
299 |
let specialize_op expr = |
|
300 |
match !Options.output with |
|
301 |
| "C" -> specialize_to_c expr |
|
302 |
| _ -> expr |
|
303 |
|
|
283 | 304 |
let rec translate_expr node ((m, si, j, d, s) as args) expr = |
305 |
let expr = specialize_op expr in |
|
284 | 306 |
match expr.expr_desc with |
285 | 307 |
| Expr_const v -> Cst v |
286 | 308 |
| Expr_ident x -> translate_ident node args x |
... | ... | |
294 | 316 |
| Expr_when (e1, _, _) -> translate_expr node args e1 |
295 | 317 |
| Expr_merge (x, _) -> raise NormalizationError |
296 | 318 |
| Expr_appl (id, e, _) when Basic_library.is_internal_fun id -> |
297 |
let id = |
|
298 |
(* need to specialize C (dis)equality operators wrt boolean type |
|
299 |
because C boolean truth value is not unique *) |
|
300 |
match !Options.output with |
|
301 |
| "C" when Types.is_bool_type expr.expr_type -> |
|
302 |
if id = "=" then "equi" else |
|
303 |
if id = "!=" then "xor" |
|
304 |
else id |
|
305 |
| _ -> id in |
|
306 | 319 |
let nd = node_from_name id in |
307 |
(match e.expr_desc with |
|
308 |
| Expr_tuple el -> Fun (node_name nd, List.map (translate_expr node args) el) |
|
309 |
| _ -> Fun (node_name nd, [translate_expr node args e])) |
|
320 |
Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e)) |
|
310 | 321 |
| Expr_ite (g,t,e) -> ( |
311 | 322 |
(* special treatment depending on the active backend. For horn backend, ite |
312 | 323 |
are preserved in expression. While they are removed for C or Java |
Also available in: Unified diff