Project

General

Profile

« Previous | Next » 

Revision 8c934ccd

Added by Pierre-Loïc Garoche about 3 years ago

lustrev seal: ongoing work on extraction as dynamical system. Still not working yet

View differences:

src/tools/seal/seal_verifier.ml
60 60 
  let sliced_nd = slice_node mems msch nd in
61 61 
  (* Format.eprintf "Sliced Node %a@." Printers.pp_node sliced_nd; *)
62 62 
  report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@.");
63 
  let sw_init, sw_sys = node_as_switched_sys mems sliced_nd in
63 

  		




  
  64
  
    
  let consts = Corelang.(List.map const_of_top (get_consts prog)) in


  		




  
  65
  
    
  let sw_init, sw_sys = node_as_switched_sys consts mems sliced_nd in


  		




  64
  66
  
    
  let pp_res =


  		




  65
  67
  
    
    (Utils.fprintf_list ~sep:"@ "


  		




  66
  68
  
    
       (fun fmt (gel, up) ->


  		












Also available in:  Unified diff