Project

General

Profile

« Previous | Next » 

Revision 782742b6

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

Merged unstable with seahorn

View differences:

src/lusic.ml
25 25 
  contents  : top_decl list;
26 26 
}
27 27 

  		




  28
  
  
    
module HeaderMod = C_backend_header.EmptyMod


  		




  29
  
  
    
module Header = C_backend_header.Main (HeaderMod)


  		




  30
  28
  
    

  		




  31
  29
  
    
(* extracts a header from a program representing module owner = dirname/basename *)


  		




  32
  30
  
    
let extract_header dirname basename prog =


  		




  ......




  83
  81
  
    
      }


  		




  84
  82
  
    
    end


  		




  85
  83
  
    

  		




  86
  
  
    
let print_lusic_to_h basename extension =


  		




  87
  
  
    
  let lusic = read_lusic basename extension in


  		




  88
  
  
    
  let header_name = basename ^ ".h" in


  		




  89
  
  
    
  let h_out = open_out header_name in


  		




  90
  
  
    
  let h_fmt = formatter_of_out_channel h_out in


  		




  91
  
  
    
  begin


  		




  92
  
  
    
    assert (not lusic.obsolete);


  		




  93
  
  
    
    (*Format.eprintf "lusic to h: %i items.@." (List.length lusic.contents);*)


  		




  94
  
  
    
    Typing.uneval_prog_generics lusic.contents;


  		




  95
  
  
    
    Clock_calculus.uneval_prog_generics lusic.contents;


  		




  96
  
  
    
    Header.print_header_from_header h_fmt (Filename.basename basename) lusic.contents;


  		




  97
  
  
    
    close_out h_out


  		




  98
  
  
    
  end


  		




  99
  
  
    

  		




  100
  84
  
    

  		












Also available in:  Unified diff