source: driver/extracted/cminor_classified_system.ml @ 3106

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File size: 1.8 KB
Line 
1open Preamble
2
3open Sets
4
5open Listb
6
7open StructuredTraces
8
9open FrontEndOps
10
11open Cminor_syntax
12
13open SmallstepExec
14
15open Extra_bool
16
17open Globalenvs
18
19open IOMonad
20
21open IO
22
23open FrontEndVal
24
25open Hide
26
27open ByteValues
28
29open GenMem
30
31open FrontEndMem
32
33open CostLabel
34
35open Proper
36
37open PositiveMap
38
39open Deqsets
40
41open Extralib
42
43open Lists
44
45open Identifiers
46
47open Integers
48
49open AST
50
51open Division
52
53open Exp
54
55open Arithmetic
56
57open Extranat
58
59open Vector
60
61open FoldStuff
62
63open BitVector
64
65open Z
66
67open BitVectorZ
68
69open Pointers
70
71open ErrorMessages
72
73open Option
74
75open Setoids
76
77open Monad
78
79open Positive
80
81open PreIdentifiers
82
83open Errors
84
85open Div_and_mod
86
87open Jmeq
88
89open Russell
90
91open Util
92
93open Bool
94
95open Relations
96
97open Nat
98
99open List
100
101open Hints_declaration
102
103open Core_notation
104
105open Pts
106
107open Logic
108
109open Types
110
111open Coqlib
112
113open Values
114
115open Events
116
117open Cminor_semantics
118
119open Cminor_abstract
120
121open Stacksize
122
123open Executions
124
125open Measurable
126
127(** val cminor_stack_ident :
128    Cminor_semantics.genv -> Cminor_abstract.cminor_state -> AST.ident **)
129let cminor_stack_ident ge s =
130  (match s with
131   | Cminor_semantics.State (x, x0, x1, x4, x5, x6, x8) ->
132     (fun _ -> assert false (* absurd case *))
133   | Cminor_semantics.Callstate (id, x, x0, x1, x2) -> (fun _ -> id)
134   | Cminor_semantics.Returnstate (x, x0, x1) ->
135     (fun _ -> assert false (* absurd case *))
136   | Cminor_semantics.Finalstate x ->
137     (fun _ -> assert false (* absurd case *))) __
138
139(** val cminor_pcs : Measurable.preclassified_system **)
140let cminor_pcs =
141  { Measurable.pcs_exec = Cminor_semantics.cminor_fullexec;
142    Measurable.pcs_labelled = (fun x ->
143    Obj.magic Cminor_abstract.cminor_labelled); Measurable.pcs_classify =
144    (fun x -> Obj.magic Cminor_abstract.cminor_classify);
145    Measurable.pcs_callee =
146    (Obj.magic (fun x x0 _ -> cminor_stack_ident x x0)) }
147
Note: See TracBrowser for help on using the repository browser.