Project

General

Profile

Revision 8c934ccd src/tools/zustre/zustre_common.ml

View differences:

src/tools/zustre/zustre_common.ml
36 36

  
37 37
let preprocess = Horn_backend.preprocess
38 38
  
39
  
39

  
40
exception UnknownFunction of (string * (Format.formatter -> unit))
40 41
(** Sorts
41 42

  
42 43
A sort is introduced for each basic type and each enumerated type.
......
349 350
       (val_to_expr v1)
350 351
       (val_to_expr v2)
351 352

  
352
       
353

  
354
    
353 355
  (* | _, [v1; v2] ->      Z3.Boolean.mk_and
354 356
   *      !ctx
355 357
   *      (val_to_expr v1)
......
357 359
   * 
358 360
   *      Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *)
359 361
  | _ -> (
360
    Format.eprintf
361
      "internal error: zustre unkown function %s@." i;
362
    assert false)
362
    let msg fmt = Format.fprintf fmt
363
                    "internal error: zustre unkown function %s (nb args = %i)@."
364
                    i (List.length vl)
365
    in
366
    raise (UnknownFunction(i, msg))
367
  )
363 368

  
364 369
           
365 370
(* Convert a value expression [v], with internal function calls only.  [pp_var]

Also available in: Unified diff