Project

General

Profile

Revision 25b4311f src/machine_code.ml

View differences:

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