source: Deliverables/D2.2/8051/src/dev_test.ml @ 1462

Last change on this file since 1462 was 1462, checked in by ayache, 8 years ago

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

File size: 1.0 KB
Line 
1
2(** A playground function for developers where they can test very specific
3    functionalities not available in the compiler.
4    It is called with the -dev option.
5    [filenames] are the file names given in the command line when calling
6    acc. *)
7
8let do_dev_test (filenames : string list) : unit =
9
10  let f filename =
11    Printf.printf "Processing %s...\n%!" filename ;
12    let target = Languages.RTL in
13    let print = false in
14    let debug = true in
15    let interpret = true in
16    let p = Languages.parse Languages.Clight filename in
17    let p = Languages.add_runtime p in 
18    let p = Languages.labelize p in
19    let ps = Languages.compile false Languages.Clight target p in
20    let f f' p = match Languages.language_of_ast p with
21      | l when l = target -> f' p
22      | _ -> ()
23    in
24    let actions =
25      [(print, Languages.save false false filename "") ;
26       (interpret, (fun p -> ignore (Languages.interpret debug p)))] in
27    List.iter (fun (b, f') -> if b then List.iter (f f') ps else ()) actions
28  in
29
30  List.iter f filenames
Note: See TracBrowser for help on using the repository browser.