source: Deliverables/D2.2/8051/src/LIN/LIN.mli @ 1462

Last change on this file since 1462 was 1462, checked in by ayache, 8 years ago

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

File size: 2.6 KB
Line 
1
2(** This module defines the abstract syntax tree of [LIN]. *)
3
4(** Compared to LTL where functions were graphs, the functions of a LIN program
5    are sequential instructions. *)
6
7type statement =
8
9  (* Unconditional branch. *)
10  | St_goto of Label.t
11
12  (* Label a statement. *)
13  | St_label of Label.t
14
15  (* Comment. *)
16  | St_comment of string
17
18  (* Emit a cost label. *)
19  | St_cost of CostLabel.t
20
21  (* Assign an integer constant to a register. Parameters are the destination
22     register, and the integer. *)
23  | St_int of I8051.register * int
24
25  (* Pop a value from the IRAM to the accumulator. *)
26  | St_pop
27
28  (* Push a value from the accumulator to the IRAM. *)
29  | St_push
30
31  (* Assign the address of a symbol to DPTR. Parameter is the symbol. *)
32  | St_addr of AST.ident
33
34  (* Move the content of the accumulator to a register. Parameters is the
35     destination register. *)
36  | St_from_acc of I8051.register
37
38  (* Move the content of a register to the accumulator. Parameters is the source
39     register. *)
40  | St_to_acc of I8051.register
41
42  (* Apply an operation on the accumulators. Parameter is the operation. *)
43  | St_opaccs of I8051.opaccs
44
45  (* Apply an unary operation on the A accumulator. Parameter is the
46     operation. *)
47  | St_op1 of I8051.op1
48
49  (* Apply a binary operation on the A accumulator. Parameters are the
50     operation, and the other source register. *)
51  | St_op2 of I8051.op2 * I8051.register
52
53  (* Set the carry flag to zero. *)
54  | St_clear_carry
55
56  (* Set the carry flag to 1. *)
57  | St_set_carry
58
59  (* Load from external memory (address in DPTR) to the accumulator. *)
60  | St_load
61
62  (* Store to external memory (address in DPTR) from the accumulator. *)
63  | St_store
64
65  (* Call to a function given its name. Parameter is the name of the
66     function. *)
67  | St_call_id of AST.ident
68
69  (* Call to a function given its address. Parameter are the registers holding
70     the address of the function. *)
71  | St_call_ptr of I8051.register * I8051.register
72
73  (* Branch on A accumulator. Parameter is the label to go to when the A
74     accumulator is not 0. *)
75  | St_condacc of Label.t
76
77  (* Transfer control to the address stored in the return address registers. *)
78  | St_return
79
80type internal_function = statement list
81
82type function_def =
83  | F_int of internal_function
84  | F_ext of AST.external_function
85
86(* A program is a list of global variables and their reserved space, a list of
87   function names and their definition, and the name of the main function. *)
88
89type program =
90    { vars   : (AST.ident * int (* size *)) list ;
91      functs : (AST.ident * function_def) list ;
92      main   : AST.ident option }
Note: See TracBrowser for help on using the repository browser.