Project

General

Profile

Revision 53206908 src/backends/Horn/horn_backend.ml

View differences:

src/backends/Horn/horn_backend.ml
111 111
let rec pp_horn_const fmt c =
112 112
  match c with
113 113
    | Const_int i    -> pp_print_int fmt i
114
    | Const_real r   -> pp_print_string fmt r
115
    | Const_float r  -> pp_print_float fmt r
114
    | Const_real (c,e,s)   -> assert false (* TODO rational pp_print_string fmt r *)
115
    (* | Const_float r  -> pp_print_float fmt r *)
116 116
    | Const_tag t    -> pp_horn_tag fmt t
117 117
    | _              -> assert false
118 118

  
......
121 121
   but an offset suffix may be added for array variables
122 122
*)
123 123
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
124
  match v with
124
  match v.value_desc with
125 125
    | Cst c         -> pp_horn_const fmt c
126 126
    | Array _
127 127
    | Access _ -> assert false (* no arrays *)
......
135 135

  
136 136
(* Prints a [value] indexed by the suffix list [loop_vars] *)
137 137
let rec pp_value_suffix self pp_value fmt value =
138
 match value with
138
 match value.value_desc with
139 139
 | Fun (n, vl)  ->
140 140
   Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
141 141
 |  _            ->
......
163 163
   	    self
164 164
   	    (pp_horn_var m)
165 165
	    fmt
166
   	    o.var_type (LocalVar o) i1
166
   	    o.var_type (mk_val (LocalVar o) o.var_type) i1
167 167
        else
168 168
          pp_assign
169 169
   	    m self (pp_horn_var m) fmt
170
   	    o.var_type (LocalVar o) i2
171

  
170
   	    o.var_type (mk_val (LocalVar o) o.var_type) i2
171
	    
172 172
      end
173 173
      | name, _, _ ->
174 174
	begin
......
181 181
	      inputs
182 182
	      (Utils.pp_final_char_if_non_empty " " inputs)
183 183
	      (* outputs *)
184
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
185
	      (List.map (fun v -> LocalVar v) outputs)
184
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) 
185
	      (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
186 186
	      (Utils.pp_final_char_if_non_empty " " outputs)
187 187
	      (* memories (next) *)
188 188
	      (Utils.fprintf_list ~sep:" " pp_var) (
......
195 195
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
196 196
	      pp_machine_step_name (node_name n)
197 197
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
198
	      (Utils.pp_final_char_if_non_empty " " inputs)
199
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
200
	      (List.map (fun v -> LocalVar v) outputs)
198
	      (Utils.pp_final_char_if_non_empty " " inputs) 
199
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) 
200
	      (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
201 201
	      (Utils.pp_final_char_if_non_empty " " outputs)
202 202
	      (Utils.fprintf_list ~sep:" " pp_var) (
203 203
		(rename_machine_list
......
218 218
	(node_name n)
219 219
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
220 220
	inputs
221
	(Utils.pp_final_char_if_non_empty " " inputs)
222
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
223
	(List.map (fun v -> LocalVar v) outputs)
221
	(Utils.pp_final_char_if_non_empty " " inputs) 
222
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) 
223
	(List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
224 224
    )
225 225

  
226 226
let pp_machine_init (m: machine_t) self fmt inst =
......
247 247
  | MLocalAssign (i,v) ->
248 248
    pp_assign
249 249
      m self (pp_horn_var m) fmt
250
      i.var_type (LocalVar i) v
250
      i.var_type (mk_val (LocalVar i) i.var_type) v
251 251
  | MStateAssign (i,v) ->
252 252
    pp_assign
253 253
      m self (pp_horn_var m) fmt
254
      i.var_type (StateVar i) v
255
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
254
      i.var_type (mk_val (StateVar i) i.var_type) v
255
  | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type)  -> 
256 256
    assert false (* This should not happen anymore *)
257 257
  | MStep (il, i, vl) ->
258 258
    pp_instance_call machines ~init:init m self fmt i vl il
......
264 264
      let el = try List.assoc tag_false hl with Not_found -> [] in
265 265
      pp_conditional machines ~init:init m self fmt g tl el
266 266
    else assert false (* enum type case *)
267
  | MComment _ -> ()
267 268

  
268 269

  
269 270
(**************************************************************)
......
362 363
                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
363 364
          end
364 365
       );
366
       
367
(*
368
       match m.mspec with
369
	 None -> () (* No node spec; we do nothing *)
370
       | Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} -> 
371
	 ( 
372
       (* For the moment, we only deal with simple case: single ensures, no other parameters *)
373
	   ()
374
	     
375
	 )
376
       | _ -> () (* Other cases give nothing *)
377
*)      
365 378
     end
366 379
    end
367 380

  
......
427 440
    (pp_conj pp_var) main_output
428 441
    (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
429 442
    ;
430
   if !Options.horn_query then Format.fprintf fmt "(query ERR)@."
443
  if !Options.horn_queries then
444
    Format.fprintf fmt "(query ERR)@."
431 445

  
432 446

  
433 447
let cex_computation machines fmt node machine =

Also available in: Unified diff