Ignore:
Timestamp:
Oct 25, 2011, 4:11:11 PM (9 years ago)
Author:
ayache
Message:

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/languages.mli

    r818 r1462  
    3434val language_of_ast : ast -> name
    3535
    36 (** [parse name] returns the parsing function of the language
    37     [name]. *)
    38 val parse : name -> (string -> ast)
     36(** [parse ?is_lustre_file ?remove_lustre_externals name] returns the parsing
     37    function of the language [name]. *)
     38val parse : ?is_lustre_file:bool -> ?remove_lustre_externals:bool ->
     39  name -> (string -> ast)
    3940
    4041(** {2 Compilation} *)
     
    6667
    6768(** [annotate input_ast target_ast] inserts cost annotations into the input AST
    68     from the (final) target AST. It also returns the name of the cost variable
    69     and the name of the cost increment function. *)
    70 val annotate : ast -> ast -> (ast * string * string)
     69    from the (final) target AST. It also returns the name of the cost variable,
     70    the name of the cost increment function, and a the name of a fresh
     71    uninitialized global variable for each external function. *)
     72val annotate : ast -> ast -> (ast * string * string * string StringTools.Map.t)
    7173
    7274(** [interpret debug ast] runs the program [ast] from the default initial
     
    7678(** {2 Serialization} *)
    7779
    78 (** [save exact_output filename input_ast] pretty prints [input_ast] in a file
    79     whose name is prefixed by [filename] and whose extension is deduced from the
    80     language of the AST. If [exact_output] is false then the written file will
    81     be fresh. *)
    82 val save : bool -> string -> string -> ast -> unit
     80(** [save asm_pretty exact_output filename input_ast] prints [input_ast] in a
     81    file whose name is prefixed by [filename] and whose extension is deduced
     82    from the language of the AST. If [exact_output] is false then the written
     83    file will be fresh. If [asm_pretty] is true, then an additional
     84    pretty-printed assembly file is output. *)
     85val save : bool -> bool -> string -> string -> ast -> unit
    8386
    84 (** [save_cost_incr filename cost_id cost_incr] prints the name [cost_id] of the
    85     cost variable and then the name [cost_incr] of the cost increment function
    86     in a seperate line in the file prefixed by [filename] and extended with
     87(** [save_cost exact_name filename cost_id cost_incr extern_cost_variables]
     88    prints the name [cost_id] of the cost variable, then the name [cost_incr] of
     89    the cost increment function, and the entries of the mapping
     90    [extern_cost_variables] (key first, then binding, seperated by a space) in a
     91    seperate line in the file prefixed by [filename] and extended with
    8792    ".cost". If the file already exists, it is overwritten. *)
    88 val save_cost : string -> string -> string -> unit
     93val save_cost : bool -> string -> string -> string ->
     94  string StringTools.Map.t -> unit
    8995
    9096(** [from_string s] parses [s] as an intermediate language name. *)
     
    9399(** [to_string n] prints [n] as a string. *)
    94100val to_string   : name -> string
     101
     102(** [add_lustre_main lustre_test lustre_test_cases lustre_test_cycles
     103    lustre_test_min_int lustre_test_max_int ast] adds a main function that tests
     104    a Lustre step function to a Clight AST. The file [lustre_test] contains
     105    CerCo information (e.g. the name of the cost variable). The integer
     106    [lustre_test_cases] is the number of test cases that are performed, and the
     107    integer [lustre_test_cycles] is the number of cycles per test
     108    case. [lustre_test_min_int] (resp. [lustre_test_max_int]) is the minimum
     109    (resp. maximum) integer value randomly generated during testing, and. *)
     110val add_lustre_main : string -> int -> int -> int -> int -> ast -> ast
Note: See TracChangeset for help on using the changeset viewer.