Project

General

Profile

Revision 51106b7e

View differences:

src/tools/zustre/zustre_cex.ml
57 57
      (* Recall that MAIN args are in@mems@out *)
58 58
      let args = Z3.Expr.get_args conj in
59 59
      if List.length args = 1 + nb_inputs + nb_mems + nb_outputs then
60
	let id = Z3.Arithmetic.Integer.get_int (List.hd args) in
60
        (* Should be done with get_int but that function vanished from the opam Z3 API *)
61
	let id = Big_int.int_of_big_int (Z3.Arithmetic.Integer.get_big_int (List.hd args)) in
61 62
	let input_values = Utils.List.extract args 1 (1 + nb_inputs) in
62 63
	let output_values = Utils.List.extract args (1+nb_inputs+nb_mems) (1 + nb_inputs + nb_mems + nb_outputs) in
63 64
	(id, (input_values, output_values))::main, funs
src/tools/zustre/zustre_common.ml
366 366
   is a printer for variables (typically [pp_c_var_read]), but an offset suffix
367 367
   may be added for array variables
368 368
*)
369
let rec horn_val_to_expr ?(is_lhs=false) self v =
369
let rec horn_val_to_expr ?(is_lhs=false) m self v =
370 370
  match v.value_desc with
371 371
  | Cst c       -> horn_const_to_expr c
372 372

  
......
393 393
            !ctx
394 394
	    (build_array (t, (x+1)))
395 395
	    (Z3.Arithmetic.Integer.mk_numeral_i !ctx x)
396
	    (horn_val_to_expr ~is_lhs:is_lhs self h)
396
	    (horn_val_to_expr ~is_lhs:is_lhs m self h)
397 397
     in
398 398
     build_array (il, 0)
399
       
399
     
400 400
  | Access(tab,index) ->
401 401
     Z3.Z3Array.mk_select !ctx 
402
       (horn_val_to_expr ~is_lhs:is_lhs self tab)
403
       (horn_val_to_expr ~is_lhs:is_lhs self index)
402
       (horn_val_to_expr ~is_lhs:is_lhs m self tab)
403
       (horn_val_to_expr ~is_lhs:is_lhs m self index)
404 404

  
405 405
  (* Code specific for arrays *)
406 406
    
407 407
  | Power (v, n)  -> assert false
408
  | LocalVar v    ->
409
     horn_var_to_expr
410
       (rename_machine
411
          self
412
          v)
413
  | StateVar v    ->
414
     if Types.is_array_type v.var_type
415
     then assert false
416
     else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
417
  | Fun (n, vl)   -> horn_basic_app n (horn_val_to_expr self) vl
408
  | Var v    ->
409
     if is_memory m v then
410
       if Types.is_array_type v.var_type
411
       then assert false
412
       else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
413
     
414
     else 
415
       horn_var_to_expr
416
         (rename_machine
417
            self
418
            v)
419
  | Fun (n, vl)   -> horn_basic_app n (horn_val_to_expr m self) vl
418 420

  
419 421
let no_reset_to_exprs machines m i =
420 422
  let (n,_) = List.assoc i m.minstances in
......
478 480
    let idx = horn_var_to_expr idx in
479 481
    let uid = uid_conc (get_instance_uid i) (horn_var_to_expr uid) in
480 482
    let inout = 
481
      List.map (horn_val_to_expr self)
482
	(inputs @ (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs))
483
      List.map (horn_val_to_expr m self)
484
	(inputs @ (List.map (fun v -> mk_val (Var v) v.var_type) outputs))
483 485
    in
484 486
    idx::uid::inout
485 487
  in
......
509 511
          let stmt1 = (* out = ite mem_m then i1 else i2 *)
510 512
            Z3.Boolean.mk_eq !ctx
511 513
              ( (* output var *)
512
                horn_val_to_expr
514
                horn_val_to_expr 
513 515
                  ~is_lhs:true
514
                  self
515
                  (mk_val (LocalVar o) o.var_type)
516
                  m self
517
                  (mk_val (Var o) o.var_type)
516 518
              )
517 519
              (
518 520
                Z3.Boolean.mk_ite !ctx 
519 521
	          (horn_var_to_expr mem_m) 
520
	          (horn_val_to_expr self i1)
521
	          (horn_val_to_expr self i2)
522
	          (horn_val_to_expr m self i1)
523
	          (horn_val_to_expr m self i2)
522 524
              )
523 525
          in
524 526
          let stmt2 = (* mem_X = false *)
......
578 580
  let e =
579 581
    Z3.Boolean.mk_eq
580 582
      !ctx
581
      (horn_val_to_expr ~is_lhs:true self var_name)
582
      (horn_val_to_expr self value)
583
      (horn_val_to_expr ~is_lhs:true m self var_name)
584
      (horn_val_to_expr m self value)
583 585
  (* was: TODO deal with array accesses       (value_suffix_to_expr self value) *)
584 586
  in
585 587
  [e]
......
598 600
  | MLocalAssign (i,v) ->
599 601
    assign_to_exprs
600 602
      m  
601
      (mk_val (LocalVar i) i.var_type) v,
603
      (mk_val (Var i) i.var_type) v,
602 604
    reset_instances
603 605
  | MStateAssign (i,v) ->
604 606
    assign_to_exprs
605 607
      m 
606
      (mk_val (StateVar i) i.var_type) v,
608
      (mk_val (Var i) i.var_type) v,
607 609
    reset_instances
608 610
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
609 611
    assert false (* This should not happen anymore *)
......
629 631
      let e =
630 632
	Z3.Boolean.mk_implies !ctx
631 633
          (Z3.Boolean.mk_eq !ctx 
632
             (horn_val_to_expr self g)
634
             (horn_val_to_expr m self g)
633 635
	     (horn_tag_to_expr tag))
634 636
          branch_def in
635 637

  
......
857 859
	     begin
858 860
	       (*Rule for step "; Stateless step rule with Assertions @.";*)
859 861
	       let body_with_asserts =
860
		 Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
862
		 Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl)
861 863
	       in
862 864
	       let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in
863 865
	       add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head)
......
915 917
	       (* Rule for step Assertions @.; *)
916 918
	       let body_with_asserts =
917 919
		 Z3.Boolean.mk_and !ctx
918
		   (horn_step_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
920
		   (horn_step_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl)
919 921
	       in
920 922
	       let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
921 923
	       add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)

Also available in: Unified diff