source: driver/extracted/rTLabs_classified_system.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: 2.4 KB
Line 
1open Preamble
2
3open Deqsets_extra
4
5open CostSpec
6
7open Sets
8
9open Listb
10
11open StructuredTraces
12
13open BitVectorTrie
14
15open Graphs
16
17open Order
18
19open Registers
20
21open FrontEndOps
22
23open RTLabs_syntax
24
25open SmallstepExec
26
27open CostLabel
28
29open Events
30
31open IOMonad
32
33open IO
34
35open Extra_bool
36
37open Coqlib
38
39open Values
40
41open FrontEndVal
42
43open Hide
44
45open ByteValues
46
47open Division
48
49open Z
50
51open BitVectorZ
52
53open Pointers
54
55open GenMem
56
57open FrontEndMem
58
59open Proper
60
61open PositiveMap
62
63open Deqsets
64
65open Extralib
66
67open Lists
68
69open Identifiers
70
71open Exp
72
73open Arithmetic
74
75open Vector
76
77open Div_and_mod
78
79open Util
80
81open FoldStuff
82
83open BitVector
84
85open Extranat
86
87open Integers
88
89open AST
90
91open Globalenvs
92
93open ErrorMessages
94
95open Option
96
97open Setoids
98
99open Monad
100
101open Jmeq
102
103open Russell
104
105open Positive
106
107open PreIdentifiers
108
109open Errors
110
111open Bool
112
113open Relations
114
115open Nat
116
117open Hints_declaration
118
119open Core_notation
120
121open Pts
122
123open Logic
124
125open Types
126
127open List
128
129open RTLabs_semantics
130
131open RTLabs_abstract
132
133open Stacksize
134
135open Executions
136
137open Measurable
138
139(** val rTLabs_stack_ident :
140    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_state -> AST.ident **)
141let rTLabs_stack_ident ge s =
142  (match s with
143   | RTLabs_semantics.State (x, x0, x1) ->
144     (fun _ -> assert false (* absurd case *))
145   | RTLabs_semantics.Callstate (id, x, x0, x1, x2, x3) -> (fun _ -> id)
146   | RTLabs_semantics.Returnstate (x, x0, x1, x2) ->
147     (fun _ -> assert false (* absurd case *))
148   | RTLabs_semantics.Finalstate x ->
149     (fun _ -> assert false (* absurd case *))) __
150
151(** val rTLabs_pcs : Measurable.preclassified_system **)
152let rTLabs_pcs =
153  { Measurable.pcs_exec = RTLabs_semantics.rTLabs_fullexec;
154    Measurable.pcs_labelled = (fun x ->
155    Obj.magic RTLabs_abstract.rTLabs_cost); Measurable.pcs_classify =
156    (fun x -> Obj.magic RTLabs_abstract.rTLabs_classify);
157    Measurable.pcs_callee =
158    (Obj.magic (fun x x0 _ -> rTLabs_stack_ident x x0)) }
159
160(** val rTLabs_ext_pcs : Measurable.preclassified_system **)
161let rTLabs_ext_pcs =
162  { Measurable.pcs_exec = RTLabs_abstract.rTLabs_ext_fullexec;
163    Measurable.pcs_labelled = (fun g s ->
164    RTLabs_abstract.rTLabs_cost (Obj.magic s).RTLabs_abstract.ras_state);
165    Measurable.pcs_classify = (fun g s ->
166    RTLabs_abstract.rTLabs_classify (Obj.magic s).RTLabs_abstract.ras_state);
167    Measurable.pcs_callee = (fun g s _ ->
168    rTLabs_stack_ident (Obj.magic g) (Obj.magic s).RTLabs_abstract.ras_state) }
169
Note: See TracBrowser for help on using the repository browser.