Project

General

Profile

« Previous | Next » 

Revision 97602f7c

Added by Guillaume Davy over 9 years ago

Correct bug when there is no precondition and change reprensentation
of boolean in ACSL

View differences:

src/backends/C/c_backend_spec.ml
72 72
  let rec aux t pp_suffix =
73 73
  match (Types.repr t).Types.tdesc with
74 74
  | Types.Tclock t'       -> aux t' pp_suffix
75
  | Types.Tbool           -> fprintf fmt "integer %s%a" var pp_suffix ()
75
  | Types.Tbool           -> fprintf fmt "boolean %s%a" var pp_suffix ()
76 76
  | Types.Treal           -> fprintf fmt "real %s%a" var pp_suffix ()
77 77
  | Types.Tint            -> fprintf fmt "integer %s%a" var pp_suffix ()
78 78
  | Types.Tarray (d, t')  ->
......
365 365
    | StateVar v    ->     
366 366
      if Types.is_array_type v.var_type
367 367
      then assert false
368
      else fprintf fmt "%s%s_reg.%a" self 
369
     (if !Options.no_pointer then "." else "->") pp_var v
368
      else fprintf fmt "%s%s_reg.%s" self 
369
     (if !Options.no_pointer then "." else "->") v.var_id
370 370
    | Fun (n, vl)   -> Format.fprintf fmt "%a" (basic_lib_pp_acsl n Machine_code.get_val_type (pp_acsl_val self pp_var)) vl
371 371
      
372 372

  
......
440 440
     despite its scalar Lustre type)
441 441
   - moreover, cast arrays variables into their original array type.
442 442
*)
443
let pp_acsl_var_read outputs fmt id =
443
let pp_acsl_var_read suffix outputs fmt id =
444 444
  if Types.is_array_type id.var_type
445 445
  then
446 446
    assert false (* no array *)
447 447
  else (
448
    if List.exists (fun o -> o.var_id = id.var_id) outputs (* id is output *)
449
    then fprintf fmt "*%s" id.var_id
450
    else fprintf fmt "%s" id.var_id
448
    (if List.exists (fun o -> o.var_id = id.var_id) outputs (* id is output *)
449
    then fprintf fmt "(*%s%s" id.var_id suffix
450
    else fprintf fmt "(%s%s" id.var_id suffix);
451
      match (Types.repr id.var_type).Types.tdesc with
452
      | Types.Tbool           -> fprintf fmt "?\\true:\\false)"
453
      | _ -> fprintf fmt ")"
451 454
  )
452 455

  
453 456
    
......
548 551
	)
549 552
    | _ -> fprintf fmt "spec_%i(%a%t);" 
550 553
      ee.muid   
551
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read outputs)) ee.mmstep_logic.step_inputs
554
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read "" outputs)) ee.mmstep_logic.step_inputs
552 555
      (fun fmt -> if stateless then fprintf fmt "" else fprintf fmt ", %s%s" (if !Options.no_pointer then "*" else "") self)
553 556
  in
554 557
  fprintf fmt "@[<v 2>/*@@ ";

Also available in: Unified diff