source: driver/extracted/lTL.ml @ 3106

Last change on this file since 3106 was 3043, checked in by sacerdot, 7 years ago

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 4.1 KB
Line 
1open Preamble
2
3open Extra_bool
4
5open Coqlib
6
7open Values
8
9open FrontEndVal
10
11open GenMem
12
13open FrontEndMem
14
15open Globalenvs
16
17open String
18
19open Sets
20
21open Listb
22
23open LabelledObjects
24
25open BitVectorTrie
26
27open Graphs
28
29open I8051
30
31open Order
32
33open Registers
34
35open CostLabel
36
37open Hide
38
39open Proper
40
41open PositiveMap
42
43open Deqsets
44
45open ErrorMessages
46
47open PreIdentifiers
48
49open Errors
50
51open Extralib
52
53open Lists
54
55open Identifiers
56
57open Integers
58
59open AST
60
61open Division
62
63open Exp
64
65open Arithmetic
66
67open Setoids
68
69open Monad
70
71open Option
72
73open Extranat
74
75open Vector
76
77open Div_and_mod
78
79open Jmeq
80
81open Russell
82
83open List
84
85open Util
86
87open FoldStuff
88
89open BitVector
90
91open Types
92
93open Bool
94
95open Relations
96
97open Nat
98
99open Hints_declaration
100
101open Core_notation
102
103open Pts
104
105open Logic
106
107open Positive
108
109open Z
110
111open BitVectorZ
112
113open Pointers
114
115open ByteValues
116
117open BackEndOps
118
119open Joint
120
121open Joint_LTL_LIN
122
123(** val lTL : Joint.graph_params **)
124let lTL =
125  Joint_LTL_LIN.lTL_LIN
126
127type ltl_program = Joint.joint_program
128
129(** val dpi1__o__byte_to_ltl_argument__o__inject :
130    (BitVector.byte, 'a1) Types.dPair -> Joint.hdw_argument Types.sig0 **)
131let dpi1__o__byte_to_ltl_argument__o__inject x2 =
132  Joint.hdw_argument_from_byte x2.Types.dpi1
133
134(** val eject__o__byte_to_ltl_argument__o__inject :
135    BitVector.byte Types.sig0 -> Joint.hdw_argument Types.sig0 **)
136let eject__o__byte_to_ltl_argument__o__inject x2 =
137  Joint.hdw_argument_from_byte (Types.pi1 x2)
138
139(** val byte_to_ltl_argument__o__inject :
140    BitVector.byte -> Joint.hdw_argument Types.sig0 **)
141let byte_to_ltl_argument__o__inject x1 =
142  Joint.hdw_argument_from_byte x1
143
144(** val dpi1__o__byte_to_ltl_argument :
145    (BitVector.byte, 'a1) Types.dPair -> Joint.hdw_argument **)
146let dpi1__o__byte_to_ltl_argument x1 =
147  Joint.hdw_argument_from_byte x1.Types.dpi1
148
149(** val eject__o__byte_to_ltl_argument :
150    BitVector.byte Types.sig0 -> Joint.hdw_argument **)
151let eject__o__byte_to_ltl_argument x1 =
152  Joint.hdw_argument_from_byte (Types.pi1 x1)
153
154(** val dpi1__o__reg_to_ltl_argument__o__inject :
155    (I8051.register, 'a1) Types.dPair -> Joint.hdw_argument Types.sig0 **)
156let dpi1__o__reg_to_ltl_argument__o__inject x2 =
157  Joint.hdw_argument_from_reg x2.Types.dpi1
158
159(** val eject__o__reg_to_ltl_argument__o__inject :
160    I8051.register Types.sig0 -> Joint.hdw_argument Types.sig0 **)
161let eject__o__reg_to_ltl_argument__o__inject x2 =
162  Joint.hdw_argument_from_reg (Types.pi1 x2)
163
164(** val reg_to_ltl_argument__o__inject :
165    I8051.register -> Joint.hdw_argument Types.sig0 **)
166let reg_to_ltl_argument__o__inject x1 =
167  Joint.hdw_argument_from_reg x1
168
169(** val dpi1__o__reg_to_ltl_argument :
170    (I8051.register, 'a1) Types.dPair -> Joint.hdw_argument **)
171let dpi1__o__reg_to_ltl_argument x1 =
172  Joint.hdw_argument_from_reg x1.Types.dpi1
173
174(** val eject__o__reg_to_ltl_argument :
175    I8051.register Types.sig0 -> Joint.hdw_argument **)
176let eject__o__reg_to_ltl_argument x1 =
177  Joint.hdw_argument_from_reg (Types.pi1 x1)
178
179(** val lTL_premain : ltl_program -> Joint.joint_closed_internal_function **)
180let lTL_premain p =
181  let l1 = Positive.One in
182  let l2 = Positive.P0 Positive.One in
183  let l3 = Positive.P1 Positive.One in
184  let res = { Joint.joint_if_luniverse = (Positive.P0 (Positive.P0
185    Positive.One)); Joint.joint_if_runiverse = Positive.One;
186    Joint.joint_if_result = (Obj.magic Types.It); Joint.joint_if_params =
187    (Obj.magic Types.It); Joint.joint_if_stacksize = Nat.O;
188    Joint.joint_if_local_stacksize = Nat.O; Joint.joint_if_code =
189    (Obj.magic (Identifiers.empty_map PreIdentifiers.LabelTag));
190    Joint.joint_if_entry = (Obj.magic l1) }
191  in
192  let res0 =
193    Joint.add_graph lTL
194      (Joint.prog_names (Joint.graph_params_to_params lTL) p) l1
195      (Joint.Sequential ((Joint.COST_LABEL p.Joint.init_cost_label),
196      (Obj.magic l2))) res
197  in
198  let res1 =
199    Joint.add_graph lTL
200      (Joint.prog_names (Joint.graph_params_to_params lTL) p) l2
201      (Joint.Sequential ((Joint.CALL ((Types.Inl
202      p.Joint.joint_prog.AST.prog_main), (Obj.magic Nat.O),
203      (Obj.magic Types.It))), (Obj.magic l3))) res0
204  in
205  let res2 =
206    Joint.add_graph lTL
207      (Joint.prog_names (Joint.graph_params_to_params lTL) p) l3 (Joint.Final
208      (Joint.GOTO l3)) res1
209  in
210  res2
211
Note: See TracBrowser for help on using the repository browser.