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