Project

General

Profile

« Previous | Next » 

Revision 9b0432bc

Added by Corentin Lauverjat over 1 year ago

  • ID 9b0432bc4c6c7165663ff1239ee93adac0a4a34d
  • Parent 9e88590e

Using deriving_ppx to derive show_ functions for the main types defined in lib/
Applying the same procedure of operator specialization taken from the C backend to Tiny
Lustrev has now a functional Tiny plugin : * -unrolling option has been renamed -duration because from an outside observer it is the length in steps of the abstract simulation * the plugin takes a JSON input file containing the bounds on input of the top node (option -bounds-input) * the plugins outputs its result in a Json format on the stdout. It can also output a {basename}_result.json file containing the result if the flag -tiny-output is provided
Adding a Tiny backend that generates Tiny code from Lustre
Repairing treatment of parsing error that was broken since transitioning from ocamlyacc to menhir

View differences:

lib/options_management.ml
111 111
      "-no-spec", Arg.Unit (fun () -> spec := "no"), "do not generate any specification";
112 112
      "-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>";
113 113
      "-c-spec", Arg.Unit (fun () -> spec := "c"), "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";
114
      "-tiny", Arg.Unit (fun () -> set_backend "tiny"), "generates Tiny output instead of C";
114 115
      (* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; *)
115 116
      "-ada", Arg.Unit (fun () -> set_backend "Ada"), "generates Ada encoding output instead of C";
116 117
      "-horn", Arg.Unit (fun () -> set_backend "horn"), "generates Horn clauses encoding output instead of C";

Also available in: Unified diff