source: Deliverables/D2.2/8051/src/checker.ml @ 1664

Last change on this file since 1664 was 1585, checked in by tranquil, 8 years ago

fighting with a bug of the translation from RTL to ERTL

File size: 1.7 KB
Line 
1let same_traces (traces : ((Languages.ast * AST.trace) list)) =
2  let compare_trace trace1 trace2 =
3    let occs_trace1 = Misc.ListExt.multi_set_of_list trace1
4    and occs_trace2 = Misc.ListExt.multi_set_of_list trace2 in
5    Misc.ListExt.assoc_diff occs_trace1 occs_trace2
6  in
7  let check_trace (_, (res1, trace1)) (_, (res2, trace2)) =
8    IntValue.Int32.eq res1 res2 &&
9    compare_trace trace1 trace2 = []
10  in
11  let print_trace lang1 lang2 ds = 
12    let string_of_value = function
13      | None -> "is not present"
14      | Some v -> Printf.sprintf "appears %d times" v
15    in 
16    let sentence (k, (v1, v2)) =
17      let k = CostLabel.string_of_cost_label ~pretty:true k in
18      Printf.sprintf "  Label %s %s in language `%s' \
19                        whereas it %s in language `%s'."
20        k (string_of_value v1) lang1 (string_of_value v2) lang2
21    in
22    String.concat "\n" (List.map sentence ds) 
23  in           
24  match Misc.ListExt.transitive_forall2 check_trace traces with
25    | None -> ()
26    | Some ((ast1, (res1, trace1)), (ast2, (res2, trace2))) ->
27      let lang1 = Languages.to_string (Languages.language_of_ast ast1)
28      and lang2 = Languages.to_string (Languages.language_of_ast ast2) in
29      let diff = compare_trace trace1 trace2 in
30      Error.global_error "during trace comparison"
31        (Printf.sprintf "%s%s"
32           (if res1 != res2 then
33               Printf.sprintf
34                 "The results of two intermediate programs differ:\n
35                  in %s it was %d, in %s it was %d\n"
36                 lang1
37                 (IntValue.Int32.to_int res1)
38                 lang2
39                 (IntValue.Int32.to_int res2) else "")
40           (Printf.sprintf "The traces of the two intermediate programs:\n%s"
41           (print_trace lang1 lang2 diff)))
Note: See TracBrowser for help on using the repository browser.