Project

General

Profile

« Previous | Next » 

Revision ea758c12

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

Commenting out unused variables

View differences:

src/tools/seal/seal_extract.ml
1117 1117
           
1118 1118
      in
1119 1119
      check_dup_up [] sw_sys;
1120
      let sw_sys =
1120
      let _ (* sw_sys *) =
1121 1121
        List.sort (fun (gl1, _) (gl2, _) ->
1122 1122
            let glid gl = List.map (fun (e,_) -> e.expr_tag) gl in
1123 1123
            
src/tools/zustre/zustre_cex.ml
153 153
  (*   if !debug then *)
154 154
  (*     Format.eprintf "FP help: %s@." (Z3.Fixedpoint.get_help !fp); *)
155 155

  
156
  let stats_entries =   Z3.Statistics.get_entries stats in
156
  (*  let _ (*stats_entries*) =   Z3.Statistics.get_entries stats in *)
157 157
  (* List.iter (fun e -> Format.eprintf "%s@.@?" *)
158 158
  (*   (Z3.Statistics.Entry.to_string e) *)
159 159
    
src/tools/zustre/zustre_common.ml
650 650
    List.fold_left (fun (instrs, resets) b ->
651 651
      let b_instrs, b_resets = branch_to_expr b in
652 652
      instrs@b_instrs, resets@b_resets 
653
    ) ([], reset_instances) hl 
653
      ) ([], reset_instances) hl
654
  | MSpec _ -> assert false
654 655

  
655 656
and instrs_to_expr machines reset_instances m instrs = 
656 657
  let instr_to_exprs rs i = instr_to_exprs machines rs m i in
......
728 729
	(fun accu e ->  FDSet.union accu (get_expr_vars e))
729 730
	FDSet.empty (Z3.Expr.get_args e)
730 731
  in
732
  (* Unsed variable. Coul;d be reintroduced 
731 733
  let extracted_vars = FDSet.elements (FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in
732 734
  let extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in
733 735
  let extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in
734

  
736
   *)
735 737
  if !debug then (
736 738
    Format.eprintf "Declaring rule: %s with variables @[<v 0>@ [%a@ ]@]@ @."
737 739
      (Z3.Expr.to_string expr)
......
939 941

  
940 942

  
941 943
(* Debug functions *)
942

  
944
(*
943 945
let rec extract_expr_fds e =
944 946
  (* Format.eprintf "@[<v 2>Extracting fundecls from expr %s@ " *)
945 947
  (*   (Z3.Expr.to_string e); *)
......
984 986
  in
985 987
  (* Format.eprintf "@]@ " *)
986 988
  ()      
987

  
989
 *)
988 990
(* Local Variables: *)
989 991
(* compile-command:"make -C ../.." *)
990 992
(* End: *)
src/tools/zustre/zustre_verifier.ml
167 167
      (* TODO
168 168
	 load deps: cf print_dep in horn_backend.ml
169 169

  
170
      *)
170
      
171 171
      if false then (
172 172
	
173 173
	let queries = Z3.Fixedpoint.parse_file !fp "nstep.smt2" in
......
232 232

  
233 233
	()	
234 234
      )
235
      else (
235
      else 
236

  
237
       *)
238

  
239
      (
236 240
	
237 241
	
238 242
	decl_sorts ();

Also available in: Unified diff