Project

General

Profile

« Previous | Next » 

Revision c6c8786b

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

kind2 output for printer. global option available

View differences:

src/options.ml
58 58
let gen_mcdc = ref false
59 59
let no_mutation_suffix = ref false
60 60

  
61
(* Algebraic loops unrolling *)
61 62
let solve_al = ref false
62 63
let al_nb_max = ref 15
63
  
64

  
65
(* Printer options *)
66
let kind2_print = ref false
67
                    
68
                  
64 69
(* Local Variables: *)
65 70
(* compile-command:"make -C .." *)
66 71
(* End: *)
src/options_management.ml
92 92
    "-print-clocks", Arg.Set print_clocks, "prints node clocks";
93 93
    "-algebraic-loop-solve", Arg.Set solve_al, "try to solve algebraic loops";
94 94
    "-algebraic-loop-max", Arg.Set_int al_nb_max, "try to solve \x1b[4mnb\x1b[0m number of algebraic loops  <default: 15>";
95
    "-kind2", Arg.Set kind2_print, "active kind2 output";
95 96
    "-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>";
96 97
    "-version", Arg.Unit print_version, " displays the version";
97 98
  ]
src/printers.ml
348 348
      stmts = nd.node_stmts @ c.stmts;
349 349
    }
350 350
  )
351
  
351

  
352
(* Printing top contract as comments in regular output and as contract
353
   in kind2 *)
352 354
let pp_contract fmt nd =    
353
  
354
  let c = node_as_contract nd in
355
  fprintf fmt "@[<v 2>(*@contract %s(%a) returns (%a);@ "
355
   let c = node_as_contract nd in
356
  fprintf fmt "@[<v 2>%scontract %s(%a) returns (%a);@ "
357
    (if !Options.kind2_print then "" else "(*@")
356 358
    nd.node_id
357 359
    pp_node_args nd.node_inputs
358 360
    pp_node_args nd.node_outputs;
359 361
  fprintf fmt "@[<v 2>let@ ";
360 362
  pp_spec fmt c;
361
  fprintf fmt "@]@ tel@ @]*)@ "        
363
  fprintf fmt "@]@ tel@ @]%s@ "
364
  (if !Options.kind2_print then "" else "*)")
362 365
    
363 366
let pp_spec_as_comment fmt (inl, outl, spec) =
364 367
  match spec with

Also available in: Unified diff