Project

General

Profile

« Previous | Next » 

Revision 380a8d33

Added by Pierre-Loïc Garoche almost 7 years ago

Solved bug in machine code generation for asserts that contain memories

View differences:

src/machine_code.ml
304 304
(*                       d : local variables             *)
305 305
(*                       s : step instructions           *)
306 306
let translate_ident node (m, si, j, d, s) id =
307
  (* Format.eprintf "trnaslating ident: %s@." id; *)
307 308
  try (* id is a node var *)
308 309
    let var_id = get_node_var id node in
309 310
    if ISet.exists (fun v -> v.var_id = id) m
310
    then mk_val (StateVar var_id) var_id.var_type
311
    else mk_val (LocalVar var_id) var_id.var_type
311
    then (
312
      (* Format.eprintf "a STATE VAR@."; *)
313
      mk_val (StateVar var_id) var_id.var_type
314
    )
315
    else (
316
      (* Format.eprintf "a LOCAL VAR@."; *)
317
      mk_val (LocalVar var_id) var_id.var_type
318
    )
312 319
  with Not_found ->
313 320
    try (* id is a constant *)
314 321
      let vdecl = (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) in
......
623 630
  assert (ISet.is_empty m0);
624 631
  assert (init0 = []);
625 632
  assert (Utils.IMap.is_empty j0);
626
  let m, init, j, locals, s = translate_eqs nd (m0, init0, j0, locals0, []) (assert_instrs@sorted_eqs) in
633
  let m, init, j, locals, s as context_with_asserts = translate_eqs nd (m0, init0, j0, locals0, []) (assert_instrs@sorted_eqs) in
627 634
  let mmap = Utils.IMap.fold (fun i n res -> (i, n)::res) j [] in
628 635
  {
629 636
    mname = nd;
......
650 657
	else
651 658
	  s
652 659
      );
653
      step_asserts = List.map (translate_expr nd init_args) nd_node_asserts;
660
      step_asserts = List.map (translate_expr nd context_with_asserts) nd_node_asserts;
654 661
    };
655 662
    mspec = nd.node_spec;
656 663
    mannot = nd.node_annot;

Also available in: Unified diff