Project

General

Profile

« Previous | Next » 

Revision e77a0fa5

Added by LĂ©lio Brun over 2 years ago

fix handling of state variables in spec expressions

View differences:

src/backends/C/c_backend_common.ml
367 367
(* Prints a value expression [v], with internal function calls only. [pp_var] is
368 368
   a printer for variables (typically [pp_c_var_read]), but an offset suffix may
369 369
   be added for array variables *)
370
let rec pp_c_val m self pp_var fmt v =
370
let rec pp_c_val ?(indirect=true) m self pp_var fmt v =
371 371
  let pp_c_val = pp_c_val m self pp_var in
372 372
  match v.value_desc with
373 373
  | Cst c ->
......
391 391
        Types.is_array_type v.var_type
392 392
        && not (Types.is_real_type v.var_type && !Options.mpfr)
393 393
      then fprintf fmt "%a" pp_var v
394
      else fprintf fmt "%s->_reg.%a" self pp_var v
394
      else fprintf fmt "%s%s_reg.%a" self (if indirect then "->" else ".") pp_var v
395 395
    else pp_var fmt v
396 396
  | Fun (n, vl) ->
397 397
    pp_basic_lib_fun (Types.is_int_type v.value_type) n pp_c_val fmt vl
src/backends/C/c_backend_common.mli
121 121
   a printer for variables (typically [pp_c_var_read]), but an offset suffix may
122 122
   be added for array variables *)
123 123
val pp_c_val :
124
  ?indirect:bool ->
124 125
  machine_t ->
125 126
  ident ->
126 127
  (formatter -> var_decl -> unit) ->
src/backends/C/c_backend_spec.ml
413 413

  
414 414
  let pp_expr ?(test_output = false) m mem fmt = function
415 415
    | Val v ->
416
      let pp = pp_c_val m mem (pp_c_var_read ~test_output m) in
416
      let pp = pp_c_val ~indirect:false m mem (pp_c_var_read ~test_output m) in
417 417
      (if not_var v
418 418
       then if Types.is_bool_type v.value_type
419 419
         then pp_bool_cast pp

Also available in: Unified diff