Changeset 1462 for Deliverables/D2.2/8051/src/languages.mli

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:

• Deliverables/D2.2/8051/src/languages.mli (modified) (4 diffs)

Deliverables/D2.2/8051/src/languages.mli

@@ -34 +34 @@
 val language_of_ast : ast -> name
 
-(** [parse name] returns the parsing function of the language
-    [name]. *)
-val parse : name -> (string -> ast) 
+(** [parse ?is_lustre_file ?remove_lustre_externals name] returns the parsing
+    function of the language [name]. *)
+val parse : ?is_lustre_file:bool -> ?remove_lustre_externals:bool ->
+  name -> (string -> ast) 
 
 (** {2 Compilation} *)
@@ -66 +67 @@
 
 (** [annotate input_ast target_ast] inserts cost annotations into the input AST
-    from the (final) target AST. It also returns the name of the cost variable
-    and the name of the cost increment function. *)
-val annotate : ast -> ast -> (ast * string * string)
+    from the (final) target AST. It also returns the name of the cost variable,
+    the name of the cost increment function, and a the name of a fresh
+    uninitialized global variable for each external function. *)
+val annotate : ast -> ast -> (ast * string * string * string StringTools.Map.t)
 
 (** [interpret debug ast] runs the program [ast] from the default initial
@@ -76 +78 @@
 (** {2 Serialization} *)
 
-(** [save exact_output filename input_ast] pretty prints [input_ast] in a file
-    whose name is prefixed by [filename] and whose extension is deduced from the
-    language of the AST. If [exact_output] is false then the written file will
-    be fresh. *)
-val save : bool -> string -> string -> ast -> unit
+(** [save asm_pretty exact_output filename input_ast] prints [input_ast] in a
+    file whose name is prefixed by [filename] and whose extension is deduced
+    from the language of the AST. If [exact_output] is false then the written
+    file will be fresh. If [asm_pretty] is true, then an additional
+    pretty-printed assembly file is output. *)
+val save : bool -> bool -> string -> string -> ast -> unit
 
-(** [save_cost_incr filename cost_id cost_incr] prints the name [cost_id] of the
-    cost variable and then the name [cost_incr] of the cost increment function
-    in a seperate line in the file prefixed by [filename] and extended with
+(** [save_cost exact_name filename cost_id cost_incr extern_cost_variables]
+    prints the name [cost_id] of the cost variable, then the name [cost_incr] of
+    the cost increment function, and the entries of the mapping
+    [extern_cost_variables] (key first, then binding, seperated by a space) in a
+    seperate line in the file prefixed by [filename] and extended with
     ".cost". If the file already exists, it is overwritten. *)
-val save_cost : string -> string -> string -> unit
+val save_cost : bool -> string -> string -> string ->
+  string StringTools.Map.t -> unit
 
 (** [from_string s] parses [s] as an intermediate language name. *)
@@ -93 +99 @@
 (** [to_string n] prints [n] as a string. *)
 val to_string   : name -> string
+
+(** [add_lustre_main lustre_test lustre_test_cases lustre_test_cycles
+    lustre_test_min_int lustre_test_max_int ast] adds a main function that tests
+    a Lustre step function to a Clight AST. The file [lustre_test] contains
+    CerCo information (e.g. the name of the cost variable). The integer
+    [lustre_test_cases] is the number of test cases that are performed, and the
+    integer [lustre_test_cycles] is the number of cycles per test
+    case. [lustre_test_min_int] (resp. [lustre_test_max_int]) is the minimum
+    (resp. maximum) integer value randomly generated during testing, and. *)
+val add_lustre_main : string -> int -> int -> int -> int -> ast -> ast