Revision 2fdbc781
Added by Pierre-Loïc Garoche about 8 years ago
| Makefile.in | ||
|---|---|---|
| 1 |
OCAMLBUILD=@OCAMLBUILD@ -classic-display -no-links |
|
| 2 |
|
|
| 3 | 1 |
prefix=@prefix@ |
| 4 | 2 |
exec_prefix=@exec_prefix@ |
| 5 | 3 |
bindir=@bindir@ |
| src/Makefile.in | ||
|---|---|---|
| 1 |
OCAMLBUILD=@OCAMLBUILD@ -classic-display -use-ocamlfind -no-links
|
|
| 1 |
OCAMLBUILD=@OCAMLBUILD@ -use-ocamlfind -no-links |
|
| 2 | 2 |
|
| 3 | 3 |
prefix=@prefix@ |
| 4 | 4 |
exec_prefix=@exec_prefix@ |
| src/backends/C/c_backend_mauve.ml | ||
|---|---|---|
| 41 | 41 |
(* -------------------------------------------------- *) |
| 42 | 42 |
|
| 43 | 43 |
let mauve_default_value v = |
| 44 |
let v_name = v.var_id in |
|
| 44 |
(* let v_name = v.var_id in *) |
|
| 45 |
|
|
| 45 | 46 |
let v_type = (Types.repr v.var_type).Types.tdesc in |
| 46 | 47 |
match v_type with |
| 47 | 48 |
| Types.Tbool -> "false" |
| src/backends/Horn/horn_backend_printers.ml | ||
|---|---|---|
| 336 | 336 |
fix here as (not a) or b *) |
| 337 | 337 |
(pp_horn_val self (pp_horn_var m)) g |
| 338 | 338 |
tag; |
| 339 |
let rs = pp_machine_instrs machines reset_instances m fmt instrs in
|
|
| 339 |
let _ (* rs *) = pp_machine_instrs machines reset_instances m fmt instrs in
|
|
| 340 | 340 |
fprintf fmt "@])"; |
| 341 | 341 |
() (* rs *) |
| 342 | 342 |
in |
| src/lustreSpec.ml | ||
|---|---|---|
| 9 | 9 |
(* *) |
| 10 | 10 |
(********************************************************************) |
| 11 | 11 |
|
| 12 |
open Format |
|
| 13 |
|
|
| 14 | 12 |
type ident = Utils.ident |
| 15 | 13 |
type rat = Utils.rat |
| 16 | 14 |
type tag = Utils.tag |
| src/main_lustre_testgen.ml | ||
|---|---|---|
| 51 | 51 |
check_stateless_decls prog; |
| 52 | 52 |
|
| 53 | 53 |
(* Typing *) |
| 54 |
let computed_types_env = type_decls type_env prog in
|
|
| 54 |
let _ (*computed_types_env*) = type_decls type_env prog in
|
|
| 55 | 55 |
|
| 56 | 56 |
(* Clock calculus *) |
| 57 |
let computed_clocks_env = clock_decls clock_env prog in
|
|
| 57 |
let _ (*computed_clocks_env*) = clock_decls clock_env prog in
|
|
| 58 | 58 |
|
| 59 | 59 |
(* Creating destination directory if needed *) |
| 60 | 60 |
create_dest_dir (); |
| src/mutation.ml | ||
|---|---|---|
| 236 | 236 |
| Expr_tuple l -> |
| 237 | 237 |
let mut, l' = select_in_list l rdm_mutate_expr in |
| 238 | 238 |
mut, mk_e (Expr_tuple l') |
| 239 |
| Expr_ite (i,t,e) -> |
|
| 240 |
let mut, [i'; t'; e'] = select_in_list [i; t; e] rdm_mutate_expr in |
|
| 241 |
mut, mk_e (Expr_ite (i', t', e')) |
|
| 242 |
| Expr_arrow (e1, e2) -> |
|
| 243 |
let mut, [e1'; e2'] = select_in_list [e1; e2] rdm_mutate_expr in |
|
| 244 |
mut, mk_e (Expr_arrow (e1', e2')) |
|
| 239 |
| Expr_ite (i,t,e) -> ( |
|
| 240 |
let mut, l = select_in_list [i; t; e] rdm_mutate_expr in |
|
| 241 |
match l with |
|
| 242 |
| [i'; t'; e'] -> mut, mk_e (Expr_ite (i', t', e')) |
|
| 243 |
| _ -> assert false |
|
| 244 |
) |
|
| 245 |
| Expr_arrow (e1, e2) -> ( |
|
| 246 |
let mut, l = select_in_list [e1; e2] rdm_mutate_expr in |
|
| 247 |
match l with |
|
| 248 |
| [e1'; e2'] -> mut, mk_e (Expr_arrow (e1', e2')) |
|
| 249 |
| _ -> assert false |
|
| 250 |
) |
|
| 245 | 251 |
| Expr_pre e -> |
| 246 | 252 |
let select_pre = Random.bool () in |
| 247 | 253 |
if select_pre then |
| src/pathConditions.ml | ||
|---|---|---|
| 59 | 59 |
let neg = List.map (compute_neg_expr cpt_pre) l in |
| 60 | 60 |
combine (fun l' -> {expr with expr_desc = Expr_tuple l'}) neg l
|
| 61 | 61 |
|
| 62 |
| Expr_ite (i,t,e) when (Types.repr t.expr_type).Types.tdesc = Types.Tbool -> |
|
| 62 |
| Expr_ite (i,t,e) when (Types.repr t.expr_type).Types.tdesc = Types.Tbool -> (
|
|
| 63 | 63 |
let list = [i; t; e] in |
| 64 | 64 |
let neg = List.map (compute_neg_expr cpt_pre) list in |
| 65 |
combine (fun [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}) neg list
|
|
| 65 |
combine (fun l -> |
|
| 66 |
match l with |
|
| 67 |
| [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}
|
|
| 68 |
| _ -> assert false |
|
| 69 |
) neg list |
|
| 70 |
) |
|
| 66 | 71 |
| Expr_ite (i,t,e) -> ( (* We return the guard as a new guard *) |
| 67 | 72 |
gen_mcdc_cond_guard i; |
| 68 | 73 |
let list = [i; t; e] in |
| 69 | 74 |
let neg = List.map (compute_neg_expr cpt_pre) list in |
| 70 |
combine (fun [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}) neg list
|
|
| 75 |
combine (fun l -> |
|
| 76 |
match l with |
|
| 77 |
| [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}
|
|
| 78 |
| _ -> assert false |
|
| 79 |
) neg list |
|
| 71 | 80 |
) |
| 72 | 81 |
| Expr_arrow (e1, e2) -> |
| 73 | 82 |
let e1' = compute_neg_expr cpt_pre e1 in |
| 74 | 83 |
let e2' = compute_neg_expr cpt_pre e2 in |
| 75 |
combine (fun [x;y] -> { expr with expr_desc = Expr_arrow (x, y) }) [e1'; e2'] [e1; e2]
|
|
| 84 |
combine (fun l -> match l with |
|
| 85 |
| [x;y] -> { expr with expr_desc = Expr_arrow (x, y) }
|
|
| 86 |
| _ -> assert false |
|
| 87 |
) [e1'; e2'] [e1; e2] |
|
| 76 | 88 |
| Expr_pre e -> |
| 77 | 89 |
List.map |
| 78 | 90 |
(fun (v, negv) -> (v, { expr with expr_desc = Expr_pre negv } ))
|
| src/plugins/salsa/machine_salsa_opt.ml | ||
|---|---|---|
| 57 | 57 |
List.fold_left (fun vars (_, b) -> Vars.union vars (get_read_vars b) ) vars branches |
| 58 | 58 |
) |
| 59 | 59 |
| LT.MReset _ |
| 60 |
| LT.MNoReset _ |
|
| 60 | 61 |
| LT.MComment _ -> Vars.empty |
| 61 | 62 |
) |
| 62 | 63 |
|
| ... | ... | |
| 73 | 74 |
List.fold_left (fun vars (_, b) -> Vars.union vars (get_written_vars b) ) vars_tl branches |
| 74 | 75 |
) |
| 75 | 76 |
| LT.MReset _ |
| 77 |
| LT.MNoReset _ |
|
| 76 | 78 |
| LT.MComment _ -> Vars.empty |
| 77 | 79 |
) |
| 78 | 80 |
|
| ... | ... | |
| 440 | 442 |
produced within branches *) |
| 441 | 443 |
|
| 442 | 444 |
|
| 443 |
| LT.MReset(_) | LT.MComment _ -> |
|
| 445 |
| LT.MReset(_) | LT.MNoReset _ | LT.MComment _ ->
|
|
| 444 | 446 |
if debug then Format.eprintf "Untouched %a (non real)@ " MC.pp_instr hd_instr; |
| 445 | 447 |
|
| 446 | 448 |
(* Untouched instruction *) |
Also available in: Unified diff
Cleaning output:
- no more classic display for ocamlc
- compilation warnings removed