Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/backends/C/c_backend_spec.ml
1

  
2 1
(********************************************************************)
3 2
(*                                                                  *)
4 3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
......
23 22

  
24 23
(**************************************************************************)
25 24

  
26
(* TODO ACSL
27
   Return updates machines (eg with local annotations) and acsl preamble *)
25
(* TODO ACSL Return updates machines (eg with local annotations) and acsl
26
   preamble *)
28 27
let preprocess_acsl machines = machines, []
29
                          
28

  
30 29
let pp_acsl_basic_type_desc t_desc =
31 30
  if Types.is_bool_type t_desc then
32 31
    (* if !Options.cpp then "bool" else "_Bool" *)
......
36 35
    if t_desc.tid = -1 then "int" else "integer"
37 36
  else if Types.is_real_type t_desc then
38 37
    if !Options.mpfr then Mpfr.mpfr_t else !Options.real_type
39
  else
40
    assert false (* Not a basic C type. Do not handle arrays or pointers *)
38
  else assert false
39
(* Not a basic C type. Do not handle arrays or pointers *)
41 40

  
42
let pp_acsl pp fmt =
43
  fprintf fmt "@[<v>/*%@ @[<v>%a@]@,*/@]" pp
41
let pp_acsl pp fmt = fprintf fmt "@[<v>/*%@ @[<v>%a@]@,*/@]" pp
44 42

  
45
let pp_acsl_cut pp fmt =
46
  fprintf fmt "%a@," (pp_acsl pp)
43
let pp_acsl_cut pp fmt = fprintf fmt "%a@," (pp_acsl pp)
47 44

  
48
let pp_acsl_line pp fmt =
49
  fprintf fmt "//%@ @[<h>%a@]" pp
45
let pp_acsl_line pp fmt = fprintf fmt "//%@ @[<h>%a@]" pp
50 46

  
51
let pp_acsl_line' pp fmt =
52
  fprintf fmt "/*%@ @[<h>%a@] */" pp
47
let pp_acsl_line' pp fmt = fprintf fmt "/*%@ @[<h>%a@] */" pp
53 48

  
54
let pp_acsl_line_cut pp fmt =
55
  fprintf fmt "%a@," (pp_acsl_line pp)
49
let pp_acsl_line_cut pp fmt = fprintf fmt "%a@," (pp_acsl_line pp)
56 50

  
57
let pp_requires pp_req fmt =
58
  fprintf fmt "requires %a;" pp_req
51
let pp_requires pp_req fmt = fprintf fmt "requires %a;" pp_req
59 52

  
60
let pp_ensures pp_ens fmt =
61
  fprintf fmt "ensures %a;" pp_ens
53
let pp_ensures pp_ens fmt = fprintf fmt "ensures %a;" pp_ens
62 54

  
63
let pp_assumes pp_asm fmt =
64
  fprintf fmt "assumes %a;" pp_asm
55
let pp_assumes pp_asm fmt = fprintf fmt "assumes %a;" pp_asm
65 56

  
66 57
let pp_assigns pp =
67 58
  pp_comma_list
68 59
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "assigns ")
69
    ~pp_epilogue:pp_print_semicolon'
70
    pp
60
    ~pp_epilogue:pp_print_semicolon' pp
71 61

  
72
let pp_ghost pp_gho fmt =
73
  fprintf fmt "ghost %a" pp_gho
62
let pp_ghost pp_gho fmt = fprintf fmt "ghost %a" pp_gho
74 63

  
75
let pp_assert pp_ast fmt =
76
  fprintf fmt "assert %a;" pp_ast
64
let pp_assert pp_ast fmt = fprintf fmt "assert %a;" pp_ast
77 65

  
78 66
let pp_mem_valid pp_var fmt (name, var) =
79 67
  fprintf fmt "%s_valid(%a)" name pp_var var
......
90 78

  
91 79
let pp_access' = pp_access pp_print_string pp_print_string
92 80

  
93
let pp_var_decl fmt v =
94
  pp_print_string fmt v.var_id
81
let pp_var_decl fmt v = pp_print_string fmt v.var_id
95 82

  
96 83
let pp_reg self fmt field =
97 84
  pp_access pp_indirect' pp_var_decl fmt ((self, "_reg"), field)
98 85

  
99
let pp_true fmt () =
100
  pp_print_string fmt "\\true"
86
let pp_true fmt () = pp_print_string fmt "\\true"
101 87

  
102
let pp_false fmt () =
103
  pp_print_string fmt "\\false"
88
let pp_false fmt () = pp_print_string fmt "\\false"
104 89

  
105
let pp_at pp_v fmt (v, l) =
106
  fprintf fmt "\\at(%a, %s)" pp_v v l
90
let pp_at pp_v fmt (v, l) = fprintf fmt "\\at(%a, %s)" pp_v v l
107 91

  
108 92
let instances machines m =
109 93
  let open List in
110 94
  let grow paths i td mems =
111 95
    match paths with
112
    | [] -> [[i, (td, mems)]]
113
    | _ -> map (cons (i, (td, mems))) paths
96
    | [] ->
97
      [ [ i, (td, mems) ] ]
98
    | _ ->
99
      map (cons (i, (td, mems))) paths
114 100
  in
115 101
  let rec aux paths m =
116
    map (fun (i, (td, _)) ->
102
    map
103
      (fun (i, (td, _)) ->
117 104
        try
118 105
          let m = find (fun m -> m.mname.node_id = node_name td) machines in
119 106
          aux (grow paths i td m.mmemory) m
120 107
        with Not_found -> grow paths i td [])
121
      m.minstances |> flatten
108
      m.minstances
109
    |> flatten
122 110
  in
123 111
  aux [] m |> map rev
124 112

  
125 113
let memories insts =
126
  List.(map (fun path ->
127
      let _, (_, mems) = hd (rev path) in
128
      map (fun mem -> path, mem) mems) insts |> flatten)
129

  
130
let pp_instance ?(indirect=true) ptr =
114
  List.(
115
    map
116
      (fun path ->
117
        let _, (_, mems) = hd (rev path) in
118
        map (fun mem -> path, mem) mems)
119
      insts
120
    |> flatten)
121

  
122
let pp_instance ?(indirect = true) ptr =
131 123
  pp_print_list
132 124
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
133 125
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
134 126
    (fun fmt (i, _) -> pp_print_string fmt i)
135 127

  
136
let pp_memory ?(indirect=true) ptr fmt (path, mem) =
128
let pp_memory ?(indirect = true) ptr fmt (path, mem) =
137 129
  pp_access
138 130
    ((if indirect then pp_indirect else pp_access)
139
       (pp_instance ~indirect ptr) pp_print_string)
140
    pp_var_decl
141
    fmt ((path, "_reg"), mem)
131
       (pp_instance ~indirect ptr)
132
       pp_print_string)
133
    pp_var_decl fmt
134
    ((path, "_reg"), mem)
142 135

  
143 136
let prefixes l =
144 137
  let rec pref acc = function
145
    | x :: l -> pref ([x] :: List.map (List.cons x) acc) l
146
    | [] -> acc
138
    | x :: l ->
139
      pref ([ x ] :: List.map (List.cons x) acc) l
140
    | [] ->
141
      acc
147 142
  in
148 143
  pref [] (List.rev l)
149 144

  
150
let powerset_instances paths =
151
  List.map prefixes paths |> List.flatten
145
let powerset_instances paths = List.map prefixes paths |> List.flatten
152 146

  
153 147
let pp_separated self mem fmt (paths, ptrs) =
154
  fprintf fmt "\\separated(@[<v>%s, %s@;%a@;%a@])"
155
    self
156
    mem
157
    (pp_comma_list
158
       ~pp_prologue:pp_print_comma'
159
       (pp_instance self))
148
  fprintf fmt "\\separated(@[<v>%s, %s@;%a@;%a@])" self mem
149
    (pp_comma_list ~pp_prologue:pp_print_comma' (pp_instance self))
160 150
    paths
161
    (pp_comma_list
162
       ~pp_prologue:pp_print_comma'
163
       pp_var_decl)
151
    (pp_comma_list ~pp_prologue:pp_print_comma' pp_var_decl)
164 152
    ptrs
165 153

  
166 154
let pp_separated' =
167 155
  pp_comma_list
168 156
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "\\separated(")
169
    ~pp_epilogue:pp_print_cpar
170
    pp_var_decl
157
    ~pp_epilogue:pp_print_cpar pp_var_decl
171 158

  
172
let pp_par pp fmt =
173
  fprintf fmt "(%a)" pp
159
let pp_par pp fmt = fprintf fmt "(%a)" pp
174 160

  
175 161
let pp_forall pp_l pp_r fmt (l, r) =
176
  fprintf fmt "@[<v 2>\\forall %a;@,%a@]"
177
    pp_l l
178
    pp_r r
162
  fprintf fmt "@[<v 2>\\forall %a;@,%a@]" pp_l l pp_r r
179 163

  
180 164
let pp_exists pp_l pp_r fmt (l, r) =
181
  fprintf fmt "@[<v 2>\\exists %a;@,%a@]"
182
    pp_l l
183
    pp_r r
165
  fprintf fmt "@[<v 2>\\exists %a;@,%a@]" pp_l l pp_r r
184 166

  
185
let pp_equal pp_l pp_r fmt (l, r) =
186
  fprintf fmt "%a == %a"
187
    pp_l l
188
    pp_r r
167
let pp_equal pp_l pp_r fmt (l, r) = fprintf fmt "%a == %a" pp_l l pp_r r
189 168

  
190
let pp_different pp_l pp_r fmt (l, r) =
191
  fprintf fmt "%a != %a"
192
    pp_l l
193
    pp_r r
169
let pp_different pp_l pp_r fmt (l, r) = fprintf fmt "%a != %a" pp_l l pp_r r
194 170

  
195 171
let pp_implies pp_l pp_r fmt (l, r) =
196
  fprintf fmt "@[<v>%a ==>@ %a@]"
197
    pp_l l
198
    pp_r r
172
  fprintf fmt "@[<v>%a ==>@ %a@]" pp_l l pp_r r
199 173

  
200
let pp_and pp_l pp_r fmt (l, r) =
201
  fprintf fmt "@[<v>%a @ && %a@]"
202
    pp_l l
203
    pp_r r
174
let pp_and pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ && %a@]" pp_l l pp_r r
204 175

  
205 176
let pp_and_l pp_v fmt =
206
  pp_print_list
207
    ~pp_open_box:pp_open_vbox0
177
  pp_print_list ~pp_open_box:pp_open_vbox0
208 178
    ~pp_sep:(fun fmt () -> fprintf fmt "@,&& ")
209
    pp_v
210
    fmt
179
    pp_v fmt
211 180

  
212
let pp_or pp_l pp_r fmt (l, r) =
213
  fprintf fmt "@[<v>%a @ || %a@]"
214
    pp_l l
215
    pp_r r
181
let pp_or pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ || %a@]" pp_l l pp_r r
216 182

  
217 183
let pp_or_l pp_v fmt =
218
  pp_print_list
219
    ~pp_open_box:pp_open_vbox0
184
  pp_print_list ~pp_open_box:pp_open_vbox0
220 185
    ~pp_sep:(fun fmt () -> fprintf fmt "@,|| ")
221
    pp_v
222
    fmt
186
    pp_v fmt
223 187

  
224
let pp_not pp fmt =
225
  fprintf fmt "!%a" pp
188
let pp_not pp fmt = fprintf fmt "!%a" pp
226 189

  
227 190
let pp_valid pp =
228 191
  pp_and_l
229
  (* pp_print_list *)
192
    (* pp_print_list *)
230 193
    (* ~pp_sep:pp_print_cut *)
231 194
    (fun fmt x -> fprintf fmt "\\valid(%a)" pp x)
232 195

  
233
let pp_old pp fmt =
234
  fprintf fmt "\\old(%a)" pp
196
let pp_old pp fmt = fprintf fmt "\\old(%a)" pp
235 197

  
236 198
let pp_ite pp_c pp_t pp_f fmt (c, t, f) =
237
  fprintf fmt "(%a @[<hov>? %a@ : %a)@]"
238
    pp_c c
239
    pp_t t
240
    pp_f f
199
  fprintf fmt "(%a @[<hov>? %a@ : %a)@]" pp_c c pp_t t pp_f f
241 200

  
242
let pp_paren pp fmt v =
243
  fprintf fmt "(%a)" pp v
201
let pp_paren pp fmt v = fprintf fmt "(%a)" pp v
244 202

  
245 203
let pp_initialization pp_mem fmt (name, mem) =
246 204
  fprintf fmt "%s_initialization(%a)" name pp_mem mem
......
251 209
  pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m
252 210

  
253 211
let pp_locals m =
254
  pp_comma_list
255
    ~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0)
256
    (pp_local m)
212
  pp_comma_list ~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0) (pp_local m)
257 213

  
258
let pp_ptr_decl fmt v =
259
  pp_ptr fmt v.var_id
214
let pp_ptr_decl fmt v = pp_ptr fmt v.var_id
260 215

  
261 216
let pp_basic_assign_spec pp_l pp_r fmt typ var_name value =
262
  if Types.is_real_type typ && !Options.mpfr
263
  then
264
    assert false
217
  if Types.is_real_type typ && !Options.mpfr then assert false
265 218
    (* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)
266
  else
267
    pp_equal pp_l pp_r fmt (var_name, value)
219
  else pp_equal pp_l pp_r fmt (var_name, value)
268 220

  
269 221
let pp_assign_spec m self_l pp_var_l indirect_l self_r pp_var_r indirect_r fmt
270 222
    (var_type, var_name, value) =
......
275 227
    match vars with
276 228
    | [] ->
277 229
      pp_basic_assign_spec
278
        (pp_value_suffix ~indirect:indirect_l m self_l var_type loop_vars pp_var_l)
279
        (pp_value_suffix ~indirect:indirect_r m self_r var_type loop_vars pp_var_r)
230
        (pp_value_suffix ~indirect:indirect_l m self_l var_type loop_vars
231
           pp_var_l)
232
        (pp_value_suffix ~indirect:indirect_r m self_r var_type loop_vars
233
           pp_var_r)
280 234
        fmt typ var_name value
281 235
    | (_d, LVar _i) :: _q ->
282 236
      assert false
283
      (* let typ' = Types.array_element_type typ in
284
       * fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
285
       *   i i i pp_c_dimension d i
286
       *   (aux typ') q *)
237
    (* let typ' = Types.array_element_type typ in
238
     * fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
239
     *   i i i pp_c_dimension d i
240
     *   (aux typ') q *)
287 241
    | (_d, LInt _r) :: _q ->
288 242
      assert false
289
      (* let typ' = Types.array_element_type typ in
290
       * let szl = Utils.enumerate (Dimension.size_const_dimension d) in
291
       * fprintf fmt "@[<v 2>{@,%a@]@,}"
292
       *   (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl *)
293
    | _ -> assert false
243
    (* let typ' = Types.array_element_type typ in
244
     * let szl = Utils.enumerate (Dimension.size_const_dimension d) in
245
     * fprintf fmt "@[<v 2>{@,%a@]@,}"
246
     *   (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl *)
247
    | _ ->
248
      assert false
294 249
  in
295
  begin
296
    reset_loop_counter ();
297
    aux var_type fmt reordered_loop_vars;
298
  end
250
  reset_loop_counter ();
251
  aux var_type fmt reordered_loop_vars
299 252

  
300
let pp_nothing fmt () =
301
  pp_print_string fmt "\\nothing"
253
let pp_nothing fmt () = pp_print_string fmt "\\nothing"
302 254

  
303 255
let pp_memory_pack_aux ?i pp_mem pp_self fmt (name, mem, self) =
304
  fprintf fmt "%s_pack%a(@[<hov>%a,@ %a@])"
305
    name
306
    (pp_print_option pp_print_int) i
307
    pp_mem mem
308
    pp_self self
256
  fprintf fmt "%s_pack%a(@[<hov>%a,@ %a@])" name
257
    (pp_print_option pp_print_int)
258
    i pp_mem mem pp_self self
309 259

  
310 260
let pp_memory_pack pp_mem pp_self fmt (mp, mem, self) =
311 261
  pp_memory_pack_aux ?i:mp.mpindex pp_mem pp_self fmt
......
313 263

  
314 264
let pp_memory_pack_aux' ?i fmt =
315 265
  pp_memory_pack_aux ?i pp_print_string pp_print_string fmt
316
let pp_memory_pack' fmt =
317
  pp_memory_pack pp_print_string pp_print_string fmt
266

  
267
let pp_memory_pack' fmt = pp_memory_pack pp_print_string pp_print_string fmt
318 268

  
319 269
let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_input pp_output fmt
320 270
    (name, inputs, locals, outputs, mem_in, mem_out) =
321 271
  let stateless = fst (get_stateless_status m) in
322
  fprintf fmt "%s_transition%a(@[<hov>%t%a%a%t%a@])"
323
    name
324
    (pp_print_option pp_print_int) i
272
  fprintf fmt "%s_transition%a(@[<hov>%t%a%a%t%a@])" name
273
    (pp_print_option pp_print_int)
274
    i
325 275
    (fun fmt -> if not stateless then pp_mem_in fmt mem_in)
326 276
    (pp_comma_list
327 277
       ~pp_prologue:(fun fmt () -> if not stateless then pp_print_comma fmt ())
328
       pp_input) inputs
278
       pp_input)
279
    inputs
329 280
    (pp_print_option (fun fmt _ ->
330 281
         pp_comma_list ~pp_prologue:pp_print_comma pp_input fmt locals))
331 282
    i
332 283
    (fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out)
333
    (pp_comma_list ~pp_prologue:pp_print_comma pp_output) outputs
284
    (pp_comma_list ~pp_prologue:pp_print_comma pp_output)
285
    outputs
334 286

  
335 287
let pp_transition m pp_mem_in pp_mem_out pp_input pp_output fmt
336 288
    (t, mem_in, mem_out) =
......
339 291

  
340 292
let pp_transition_aux' ?i m =
341 293
  pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_var_decl
294

  
342 295
let pp_transition_aux'' ?i m =
343 296
  pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
297

  
344 298
let pp_transition' m =
345 299
  pp_transition m pp_print_string pp_print_string pp_var_decl pp_var_decl
300

  
346 301
let pp_transition'' m =
347 302
  pp_transition m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
348 303

  
349 304
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
350
  fprintf fmt "%s_reset_cleared(@[<hov>%a,@ %a@])"
351
    name
352
    pp_mem_in mem_in
305
  fprintf fmt "%s_reset_cleared(@[<hov>%a,@ %a@])" name pp_mem_in mem_in
353 306
    pp_mem_out mem_out
354 307

  
355 308
let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string
......
357 310
let pp_functional_update mems fmt mem =
358 311
  let rec aux fmt mems =
359 312
    match mems with
360
    | [] -> pp_print_string fmt mem
313
    | [] ->
314
      pp_print_string fmt mem
361 315
    | x :: mems ->
362 316
      fprintf fmt "{ @[<hov>%a@ \\with ._reg.%s = %s@] }" aux mems x x
363 317
  in
364 318
  aux fmt
365
  (* if Utils.ISet.is_empty mems then
366
   *   pp_print_string fmt mem
367
   *     else
368
   *   fprintf fmt "{ %s @[<hov>\\with %a@] }"
369
   *     mem
370
   *     (pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@;<1 -6>\\with ")
371
   *        (fun fmt x -> fprintf fmt "._reg.%s = %s" x x)) *)
372
      (Utils.ISet.elements mems)
319
    (* if Utils.ISet.is_empty mems then
320
     *   pp_print_string fmt mem
321
     *     else
322
     *   fprintf fmt "{ %s @[<hov>\\with %a@] }"
323
     *     mem
324
     *     (pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@;<1 -6>\\with ")
325
     *        (fun fmt x -> fprintf fmt "._reg.%s = %s" x x)) *)
326
    (Utils.ISet.elements mems)
373 327

  
374 328
module PrintSpec = struct
375

  
376 329
  type mode =
377 330
    | MemoryPackMode
378 331
    | TransitionMode
......
387 340
    | StateVar x ->
388 341
      fprintf fmt "%s.%a" mem pp_var_decl x
389 342

  
390
  let pp_expr:
391
    type a. ?output:bool -> machine_t -> ident -> formatter
392
    -> (value_t, a) expression_t -> unit =
393
    fun ?(output=false) m mem fmt -> function
394
    | Val v -> pp_c_val m mem (pp_c_var_read ~test_output:output m) fmt v
395
    | Tag t -> pp_print_string fmt t
396
    | Var v -> pp_var_decl fmt v
397
    | Memory r -> pp_reg mem fmt r
343
  let pp_expr :
344
      type a.
345
      ?output:bool ->
346
      machine_t ->
347
      ident ->
348
      formatter ->
349
      (value_t, a) expression_t ->
350
      unit =
351
   fun ?(output = false) m mem fmt -> function
352
    | Val v ->
353
      pp_c_val m mem (pp_c_var_read ~test_output:output m) fmt v
354
    | Tag t ->
355
      pp_print_string fmt t
356
    | Var v ->
357
      pp_var_decl fmt v
358
    | Memory r ->
359
      pp_reg mem fmt r
398 360

  
399 361
  let pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p =
400
    let output, mem_update = match mode with
401
      | InstrMode _ -> true, false
402
      | TransitionFootprintMode -> false, true
403
      | _ -> false, false
362
    let output, mem_update =
363
      match mode with
364
      | InstrMode _ ->
365
        true, false
366
      | TransitionFootprintMode ->
367
        false, true
368
      | _ ->
369
        false, false
404 370
    in
405
    let pp_expr:
406
      type a. ?output:bool -> formatter -> (value_t, a) expression_t -> unit =
407
      fun ?output fmt e -> pp_expr ?output m mem_out fmt e
371
    let pp_expr :
372
        type a. ?output:bool -> formatter -> (value_t, a) expression_t -> unit =
373
     fun ?output fmt e -> pp_expr ?output m mem_out fmt e
408 374
    in
409 375
    match p with
410 376
    | Transition (f, inst, i, inputs, locals, outputs, r, mems) ->
411
      let pp_mem_in, pp_mem_out = match inst with
377
      let pp_mem_in, pp_mem_out =
378
        match inst with
412 379
        | None ->
413
          pp_print_string,
414
          if mem_update then pp_functional_update mems else pp_print_string
380
          ( pp_print_string,
381
            if mem_update then pp_functional_update mems else pp_print_string )
415 382
        | Some inst ->
416
          (fun fmt mem_in ->
417
             if r then pp_print_string fmt mem_in
418
             else pp_access' fmt (mem_in, inst)),
419
          (fun fmt mem_out -> pp_access' fmt (mem_out, inst))
383
          ( (fun fmt mem_in ->
384
              if r then pp_print_string fmt mem_in
385
              else pp_access' fmt (mem_in, inst)),
386
            fun fmt mem_out -> pp_access' fmt (mem_out, inst) )
420 387
      in
421
      pp_transition_aux ?i m pp_mem_in pp_mem_out pp_expr (pp_expr ~output)
422
        fmt
388
      pp_transition_aux ?i m pp_mem_in pp_mem_out pp_expr (pp_expr ~output) fmt
423 389
        (f, inputs, locals, outputs, mem_in', mem_out')
424 390
    | Reset (_f, inst, r) ->
425 391
      pp_ite
......
429 395
        fmt
430 396
        (r, (mem_out, 1), (mem_out, (mem_in, inst)))
431 397
    | MemoryPack (f, inst, i) ->
432
      let pp_mem, pp_self = match inst with
398
      let pp_mem, pp_self =
399
        match inst with
433 400
        | None ->
434 401
          pp_print_string, pp_print_string
435 402
        | Some inst ->
436
          (fun fmt mem -> pp_access' fmt (mem, inst)),
437
          (fun fmt self -> pp_indirect' fmt (self, inst))
403
          ( (fun fmt mem -> pp_access' fmt (mem, inst)),
404
            fun fmt self -> pp_indirect' fmt (self, inst) )
438 405
      in
439 406
      pp_memory_pack_aux ?i pp_mem pp_self fmt (f, mem_out, mem_in)
440 407
    | ResetCleared f ->
441 408
      pp_reset_cleared' fmt (f, mem_in, mem_out)
442
      (* fprintf fmt "ResetCleared_%a" pp_print_string f *)
443
    | Initialization -> ()
409
    (* fprintf fmt "ResetCleared_%a" pp_print_string f *)
410
    | Initialization ->
411
      ()
444 412

  
445 413
  let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool
446 414

  
447
  let val_of_expr: type a. (value_t, a) expression_t -> value_t = function
448
    | Val v -> v
449
    | Tag t -> id_to_tag t
450
    | Var v -> vdecl_to_val v
451
    | Memory (StateVar v) -> vdecl_to_val v
452
    | Memory ResetFlag -> vdecl_to_val reset_flag
415
  let val_of_expr : type a. (value_t, a) expression_t -> value_t = function
416
    | Val v ->
417
      v
418
    | Tag t ->
419
      id_to_tag t
420
    | Var v ->
421
      vdecl_to_val v
422
    | Memory (StateVar v) ->
423
      vdecl_to_val v
424
    | Memory ResetFlag ->
425
      vdecl_to_val reset_flag
453 426

  
454 427
  let find_arrow m =
455
    try
456
      List.find (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances
457
      |> fst
458
    with Not_found -> eprintf "Internal error: arrow not found"; raise Not_found
428
    try List.find (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances |> fst
429
    with Not_found ->
430
      eprintf "Internal error: arrow not found";
431
      raise Not_found
459 432

  
460 433
  let pp_spec mode m fmt f =
461 434
    let rec pp_spec mode fmt f =
......
479 452
        | InstrMode self ->
480 453
          let mem = "*" ^ mem in
481 454
          fprintf str_formatter "%a" (pp_at pp_print_string) (mem, reset_label);
482
          self, flush_str_formatter (), false,
483
          mem, mem, false
455
          self, flush_str_formatter (), false, mem, mem, false
484 456
      in
485
      let pp_expr: type a. formatter -> (value_t, a) expression_t -> unit =
486
        fun fmt e -> pp_expr m mem_out fmt e
457
      let pp_expr : type a. formatter -> (value_t, a) expression_t -> unit =
458
       fun fmt e -> pp_expr m mem_out fmt e
487 459
      in
488 460
      let pp_spec' = pp_spec mode in
489 461
      match f with
......
492 464
      | False ->
493 465
        pp_false fmt ()
494 466
      | Equal (a, b) ->
495
        pp_assign_spec m
496
          mem_out (pp_c_var_read ~test_output:false m) indirect_l
497
          mem_in (pp_c_var_read ~test_output:false m) indirect_r
498
          fmt
467
        pp_assign_spec m mem_out
468
          (pp_c_var_read ~test_output:false m)
469
          indirect_l mem_in
470
          (pp_c_var_read ~test_output:false m)
471
          indirect_r fmt
499 472
          (type_of_l_value a, val_of_expr a, val_of_expr b)
500 473
      | And fs ->
501 474
        pp_and_l pp_spec' fmt fs
......
513 486
        pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p
514 487
      | StateVarPack ResetFlag ->
515 488
        let r = vdecl_to_val reset_flag in
516
        pp_assign_spec m
517
          mem_out (pp_c_var_read ~test_output:false m) indirect_l
518
          mem_in (pp_c_var_read ~test_output:false m) indirect_r
519
          fmt
489
        pp_assign_spec m mem_out
490
          (pp_c_var_read ~test_output:false m)
491
          indirect_l mem_in
492
          (pp_c_var_read ~test_output:false m)
493
          indirect_r fmt
520 494
          (Type_predef.type_bool, r, r)
521 495
      | StateVarPack (StateVar v) ->
522 496
        let v' = vdecl_to_val v in
523 497
        let inst = find_arrow m in
524
        pp_par (pp_implies
525
                  (pp_not (pp_initialization pp_access'))
526
                  (pp_assign_spec m
527
                     mem_out (pp_c_var_read ~test_output:false m) indirect_l
528
                     mem_in (pp_c_var_read ~test_output:false m) indirect_r))
498
        pp_par
499
          (pp_implies
500
             (pp_not (pp_initialization pp_access'))
501
             (pp_assign_spec m mem_out
502
                (pp_c_var_read ~test_output:false m)
503
                indirect_l mem_in
504
                (pp_c_var_read ~test_output:false m)
505
                indirect_r))
529 506
          fmt
530
          ((Arrow.arrow_id, (mem_out, inst)),
531
           (v.var_type, v', v'))
507
          ((Arrow.arrow_id, (mem_out, inst)), (v.var_type, v', v'))
532 508
      | ExistsMem (f, rc, tr) ->
533 509
        pp_exists
534 510
          (pp_machine_decl' ~ghost:true)
535 511
          (pp_and (pp_spec ResetOut) (pp_spec ResetIn))
536 512
          fmt
537
          ((f, mk_mem_reset m),
538
           (rc, tr))
513
          ((f, mk_mem_reset m), (rc, tr))
539 514
    in
540 515
    match mode with
541 516
    | TransitionFootprintMode ->
......
543 518
      let mem_out = mk_mem_out m in
544 519
      pp_forall
545 520
        (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
546
        (pp_spec mode)
547
        fmt ((m.mname.node_id, [mem_in; mem_out]), f)
521
        (pp_spec mode) fmt
522
        ((m.mname.node_id, [ mem_in; mem_out ]), f)
548 523
    | _ ->
549 524
      pp_spec mode fmt f
550

  
551 525
end
552 526

  
553 527
let pp_predicate pp_l pp_r fmt (l, r) =
554
  fprintf fmt "@[<v 2>predicate %a =@,%a;@]"
555
    pp_l l
556
    pp_r r
528
  fprintf fmt "@[<v 2>predicate %a =@,%a;@]" pp_l l pp_r r
557 529

  
558 530
let pp_lemma pp_l pp_r fmt (l, r) =
559
  fprintf fmt "@[<v 2>lemma %a:@,%a;@]"
560
    pp_l l
561
    pp_r r
531
  fprintf fmt "@[<v 2>lemma %a:@,%a;@]" pp_l l pp_r r
562 532

  
563 533
let pp_mem_valid_def fmt m =
564 534
  if not (fst (get_stateless_status m)) then
......
570 540
         (pp_and
571 541
            (pp_and_l (fun fmt (inst, (td, _)) ->
572 542
                 if Arrow.td_is_arrow td then
573
                   pp_valid pp_indirect' fmt [self, inst]
574
                 else
575
                   pp_mem_valid pp_indirect' fmt (node_name td, (self, inst))))
543
                   pp_valid pp_indirect' fmt [ self, inst ]
544
                 else pp_mem_valid pp_indirect' fmt (node_name td, (self, inst))))
576 545
            (pp_valid pp_print_string)))
577 546
      fmt
578
      ((name, (name, self)),
579
       (m.minstances, [self]))
547
      ((name, (name, self)), (m.minstances, [ self ]))
580 548

  
581 549
let pp_memory_pack_def m fmt mp =
582 550
  let name = mp.mpname.node_id in
......
587 555
       (pp_memory_pack (pp_machine_decl' ~ghost:true) (pp_machine_decl pp_ptr))
588 556
       (PrintSpec.pp_spec MemoryPackMode m))
589 557
    fmt
590
    ((mp, (name, mem), (name, self)),
591
     mp.mpformula)
558
    ((mp, (name, mem), (name, self)), mp.mpformula)
592 559

  
593 560
let print_machine_ghost_struct fmt m =
594 561
  pp_acsl (pp_ghost (print_machine_struct ~ghost:true)) fmt m
595 562

  
596 563
let pp_memory_pack_defs fmt m =
597 564
  if not (fst (get_stateless_status m)) then
598
    fprintf fmt "%a@,%a"
599
      print_machine_ghost_struct m
600
      (pp_print_list
601
         ~pp_epilogue:pp_print_cut
602
         ~pp_open_box:pp_open_vbox0
603
         (pp_memory_pack_def m)) m.mspec.mmemory_packs
565
    fprintf fmt "%a@,%a" print_machine_ghost_struct m
566
      (pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
567
         (pp_memory_pack_def m))
568
      m.mspec.mmemory_packs
604 569

  
605 570
let pp_transition_def m fmt t =
606 571
  let name = t.tname.node_id in
......
609 574
  pp_acsl
610 575
    (pp_predicate
611 576
       (pp_transition m
612
          (pp_machine_decl' ~ghost:true) (pp_machine_decl' ~ghost:true)
613
          (pp_local m)
614
          (pp_local m))
577
          (pp_machine_decl' ~ghost:true)
578
          (pp_machine_decl' ~ghost:true)
579
          (pp_local m) (pp_local m))
615 580
       (PrintSpec.pp_spec TransitionMode m))
616 581
    fmt
617
    ((t, (name, mem_in), (name, mem_out)),
618
     t.tformula)
582
    ((t, (name, mem_in), (name, mem_out)), t.tformula)
619 583

  
620 584
let pp_transition_defs fmt m =
621
  pp_print_list
622
    ~pp_epilogue:pp_print_cut
623
    ~pp_open_box:pp_open_vbox0
585
  pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
624 586
    (pp_transition_def m) fmt m.mspec.mtransitions
625 587

  
626 588
let pp_transition_footprint fmt t =
627
  fprintf fmt "%s_transition%a_footprint"
628
    t.tname.node_id
629
    (pp_print_option pp_print_int) t.tindex
589
  fprintf fmt "%s_transition%a_footprint" t.tname.node_id
590
    (pp_print_option pp_print_int)
591
    t.tindex
630 592

  
631 593
let pp_transition_footprint_lemma m fmt t =
632 594
  let open Utils.ISet in
633 595
  let name = t.tname.node_id in
634
  let mems = diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tfootprint in
635
  let memories = List.map (fun v ->
636
      { v with var_type = { v.var_type with tid = -1 }})
596
  let mems =
597
    diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tfootprint
598
  in
599
  let memories =
600
    List.map
601
      (fun v -> { v with var_type = { v.var_type with tid = -1 } })
637 602
      (List.filter (fun v -> not (mem v.var_id t.tfootprint)) m.mmemory)
638 603
  in
639 604
  if not (is_empty mems) then
640 605
    pp_acsl
641
      (pp_lemma
642
         pp_transition_footprint
606
      (pp_lemma pp_transition_footprint
643 607
         (PrintSpec.pp_spec TransitionFootprintMode m))
644 608
      fmt
645
      (t,
646
       Forall (
647
         memories @ t.tinputs @ t.tlocals @ t.toutputs,
648
         Imply (Spec_common.mk_transition ?i:t.tindex name
649
                  (vdecls_to_vals t.tinputs)
650
                  (vdecls_to_vals t.tlocals)
609
      ( t,
610
        Forall
611
          ( memories @ t.tinputs @ t.tlocals @ t.toutputs,
612
            Imply
613
              ( Spec_common.mk_transition ?i:t.tindex name
614
                  (vdecls_to_vals t.tinputs) (vdecls_to_vals t.tlocals)
651 615
                  (vdecls_to_vals t.toutputs),
652 616
                Spec_common.mk_transition ~mems ?i:t.tindex name
653
                  (vdecls_to_vals t.tinputs)
654
                  (vdecls_to_vals t.tlocals)
655
                  (vdecls_to_vals t.toutputs))))
617
                  (vdecls_to_vals t.tinputs) (vdecls_to_vals t.tlocals)
618
                  (vdecls_to_vals t.toutputs) ) ) )
656 619

  
657 620
let pp_transition_footprint_lemmas fmt m =
658
  pp_print_list
659
    ~pp_epilogue:pp_print_cut
660
    ~pp_open_box:pp_open_vbox0
661
    (pp_transition_footprint_lemma m) fmt
662
    (List.filter (fun t -> match t.tindex with Some i when i > 0 -> true | _ -> false)
663
         m.mspec.mtransitions)
621
  pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
622
    (pp_transition_footprint_lemma m)
623
    fmt
624
    (List.filter
625
       (fun t -> match t.tindex with Some i when i > 0 -> true | _ -> false)
626
       m.mspec.mtransitions)
664 627

  
665 628
let pp_initialization_def fmt m =
666 629
  if not (fst (get_stateless_status m)) then
......
673 636
              if Arrow.td_is_arrow td then
674 637
                pp_initialization pp_access' fmt (node_name td, (mem_in, i))
675 638
              else
676
                pp_equal (pp_reset_flag ~indirect:false pp_access') pp_print_int
677
                  fmt
639
                pp_equal
640
                  (pp_reset_flag ~indirect:false pp_access')
641
                  pp_print_int fmt
678 642
                  ((mem_in, i), 1))))
679 643
      fmt
680 644
      ((name, (name, mem_in)), m.minstances)
......
687 651
    pp_acsl
688 652
      (pp_predicate
689 653
         (pp_reset_cleared
690
            (pp_machine_decl' ~ghost:true) (pp_machine_decl' ~ghost:true))
654
            (pp_machine_decl' ~ghost:true)
655
            (pp_machine_decl' ~ghost:true))
691 656
         (pp_ite
692 657
            (pp_reset_flag' ~indirect:false)
693 658
            (pp_and
......
695 660
               pp_initialization')
696 661
            (pp_equal pp_print_string pp_print_string)))
697 662
      fmt
698
      ((name, (name, mem_in), (name, mem_out)),
699
       (mem_in,
700
        ((mem_out, 0), (name, mem_out)),
701
        (mem_out, mem_in)))
663
      ( (name, (name, mem_in), (name, mem_out)),
664
        (mem_in, ((mem_out, 0), (name, mem_out)), (mem_out, mem_in)) )
702 665

  
703
let pp_at pp_p fmt (p, l) =
704
  fprintf fmt "\\at(%a, %s)" pp_p p l
666
let pp_at pp_p fmt (p, l) = fprintf fmt "\\at(%a, %s)" pp_p p l
705 667

  
706 668
let label_pre = "Pre"
707 669

  
708
let pp_at_pre pp_p fmt p =
709
  pp_at pp_p fmt (p, label_pre)
670
let pp_at_pre pp_p fmt p = pp_at pp_p fmt (p, label_pre)
710 671

  
711
let pp_register_chain ?(indirect=true) ptr =
672
let pp_register_chain ?(indirect = true) ptr =
712 673
  pp_print_list
713 674
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
714
    ~pp_epilogue:(fun fmt () -> fprintf fmt "%s_reg._first"
715
                     (if indirect then "->" else "."))
675
    ~pp_epilogue:(fun fmt () ->
676
      fprintf fmt "%s_reg._first" (if indirect then "->" else "."))
716 677
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
717 678
    (fun fmt (i, _) -> pp_print_string fmt i)
718 679

  
719
let pp_reset_flag_chain ?(indirect=true) ptr fmt mems =
680
let pp_reset_flag_chain ?(indirect = true) ptr fmt mems =
720 681
  pp_print_list
721 682
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
722 683
    ~pp_epilogue:(fun fmt () -> pp_reset_flag' ~indirect fmt "")
......
727 688
let pp_arrow_reset_ghost mem fmt inst =
728 689
  fprintf fmt "%s_reset_ghost(%a)" Arrow.arrow_id pp_indirect' (mem, inst)
729 690

  
730
module GhostProto: MODIFIERS_GHOST_PROTO = struct
731
  let pp_ghost_parameters ?(cut=true) fmt vs =
691
module GhostProto : MODIFIERS_GHOST_PROTO = struct
692
  let pp_ghost_parameters ?(cut = true) fmt vs =
732 693
    fprintf fmt "%a%a"
733
      (if cut then pp_print_cut else pp_print_nothing) ()
694
      (if cut then pp_print_cut else pp_print_nothing)
695
      ()
734 696
      (pp_acsl_line'
735
         (pp_ghost
736
            (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x))))
697
         (pp_ghost (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x))))
737 698
      vs
738 699
end
739 700

  
740 701
module HdrMod = struct
741

  
742 702
  module GhostProto = GhostProto
743 703

  
744
  let print_machine_decl_prefix = fun _ _ -> ()
704
  let print_machine_decl_prefix _ _ = ()
745 705

  
746 706
  let pp_import_arrow fmt () =
747 707
    fprintf fmt "#include \"%s/arrow_spec.h%s\""
748 708
      (Arrow.arrow_top_decl ()).top_decl_owner
749 709
      (if !Options.cpp then "pp" else "")
750

  
751 710
end
752 711

  
753 712
module SrcMod = struct
754

  
755 713
  module GhostProto = GhostProto
756 714

  
757 715
  let pp_predicates (* dependencies *) fmt machines =
758 716
    let pp_preds comment pp =
759
      pp_print_list
760
        ~pp_open_box:pp_open_vbox0
761
        ~pp_prologue:(pp_print_endcut comment)
762
        pp
763
        ~pp_epilogue:pp_print_cutcut in
764
    fprintf fmt
765
      "%a%a%a%a%a%a"
766
      (pp_preds "/* ACSL `valid` predicates */"
767
         pp_mem_valid_def) machines
768
      (pp_preds "/* ACSL `memory pack` simulations */"
769
         pp_memory_pack_defs) machines
770
      (pp_preds "/* ACSL initialization annotations */"
771
         pp_initialization_def) machines
772
      (pp_preds "/* ACSL reset cleared annotations */"
773
         pp_reset_cleared_def) machines
774
      (pp_preds "/* ACSL transition annotations */"
775
         pp_transition_defs) machines
717
      pp_print_list ~pp_open_box:pp_open_vbox0
718
        ~pp_prologue:(pp_print_endcut comment) pp ~pp_epilogue:pp_print_cutcut
719
    in
720
    fprintf fmt "%a%a%a%a%a%a"
721
      (pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def)
722
      machines
723
      (pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
724
      machines
725
      (pp_preds "/* ACSL initialization annotations */" pp_initialization_def)
726
      machines
727
      (pp_preds "/* ACSL reset cleared annotations */" pp_reset_cleared_def)
728
      machines
729
      (pp_preds "/* ACSL transition annotations */" pp_transition_defs)
730
      machines
776 731
      (pp_preds "/* ACSL transition memory footprints lemmas */"
777
         pp_transition_footprint_lemmas) machines
732
         pp_transition_footprint_lemmas)
733
      machines
778 734

  
779 735
  let pp_clear_reset_spec fmt self mem m =
780 736
    let name = m.mname.node_id in
781
    let arws, narws = List.partition (fun (_, (td, _)) -> Arrow.td_is_arrow td)
782
        m.minstances in
783
    let mk_insts = List.map (fun x -> [x]) in
784
    pp_acsl_cut (fun fmt () ->
737
    let arws, narws =
738
      List.partition (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances
739
    in
740
    let mk_insts = List.map (fun x -> [ x ]) in
741
    pp_acsl_cut
742
      (fun fmt () ->
785 743
        fprintf fmt
786
          "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,\
787
          @[<v 2>behavior reset:@;\
788
          %a@,%a@]@,\
789
          @[<v 2>behavior no_reset:@;\
790
          %a@,%a@]@,\
791
          complete behaviors;@,\
792
          disjoint behaviors;"
793
          (pp_requires pp_mem_valid') (name, self)
794
          (pp_requires (pp_separated self mem)) (mk_insts m.minstances, [])
744
          "%a@,\
745
           %a@,\
746
           %a@,\
747
           %a@,\
748
           %a@,\
749
           %a@,\
750
           %a@,\
751
           %a@,\
752
           %a@,\
753
           %a@,\
754
           @[<v 2>behavior reset:@;\
755
           %a@,\
756
           %a@]@,\
757
           @[<v 2>behavior no_reset:@;\
758
           %a@,\
759
           %a@]@,\
760
           complete behaviors;@,\
761
           disjoint behaviors;"
762
          (pp_requires pp_mem_valid')
763
          (name, self)
764
          (pp_requires (pp_separated self mem))
765
          (mk_insts m.minstances, [])
795 766
          (pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
796 767
          (name, mem, self)
797
          (pp_ensures (pp_memory_pack_aux
798
                         ~i:(List.length m.mspec.mmemory_packs - 2)
799
                         pp_ptr pp_print_string))
768
          (pp_ensures
769
             (pp_memory_pack_aux
770
                ~i:(List.length m.mspec.mmemory_packs - 2)
771
                pp_ptr pp_print_string))
800 772
          (name, mem, self)
801
          (pp_assigns pp_reset_flag') [self]
802
          (pp_assigns (pp_register_chain self)) (mk_insts arws)
803
          (pp_assigns (pp_reset_flag_chain self)) (mk_insts narws)
804
          (pp_assigns pp_reset_flag') [mem]
805
          (pp_assigns (pp_register_chain ~indirect:false mem)) (mk_insts arws)
806
          (pp_assigns (pp_reset_flag_chain ~indirect:false mem)) (mk_insts narws)
807
          (pp_assumes (pp_equal pp_reset_flag' pp_print_int)) (mem, 1)
808
          (pp_ensures (pp_initialization pp_ptr)) (name, mem)
809
          (pp_assumes (pp_equal pp_reset_flag' pp_print_int)) (mem, 0)
810
          (pp_ensures (pp_equal pp_ptr (pp_old pp_ptr))) (mem, mem)
811
      )
773
          (pp_assigns pp_reset_flag')
774
          [ self ]
775
          (pp_assigns (pp_register_chain self))
776
          (mk_insts arws)
777
          (pp_assigns (pp_reset_flag_chain self))
778
          (mk_insts narws)
779
          (pp_assigns pp_reset_flag')
780
          [ mem ]
781
          (pp_assigns (pp_register_chain ~indirect:false mem))
782
          (mk_insts arws)
783
          (pp_assigns (pp_reset_flag_chain ~indirect:false mem))
784
          (mk_insts narws)
785
          (pp_assumes (pp_equal pp_reset_flag' pp_print_int))
786
          (mem, 1)
787
          (pp_ensures (pp_initialization pp_ptr))
788
          (name, mem)
789
          (pp_assumes (pp_equal pp_reset_flag' pp_print_int))
790
          (mem, 0)
791
          (pp_ensures (pp_equal pp_ptr (pp_old pp_ptr)))
792
          (mem, mem))
812 793
      fmt ()
813 794

  
814 795
  let pp_set_reset_spec fmt self mem m =
815 796
    let name = m.mname.node_id in
816
    pp_acsl_cut (fun fmt () ->
817
        fprintf fmt
818
          "%a@,%a@,%a"
819
          (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string)) (name, mem, self)
820
          (pp_ensures (pp_equal pp_reset_flag' pp_print_int)) (mem, 1)
821
          (pp_assigns pp_reset_flag') [self; mem])
797
    pp_acsl_cut
798
      (fun fmt () ->
799
        fprintf fmt "%a@,%a@,%a"
800
          (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
801
          (name, mem, self)
802
          (pp_ensures (pp_equal pp_reset_flag' pp_print_int))
803
          (mem, 1)
804
          (pp_assigns pp_reset_flag')
805
          [ self; mem ])
822 806
      fmt ()
823 807

  
824 808
  let pp_step_spec fmt machines self mem m =
825 809
    let name = m.mname.node_id in
826 810
    let insts = instances machines m in
827 811
    let insts' = powerset_instances insts in
828
    let insts'' = List.(filter (fun l -> l <> [])
829
                          (map (filter (fun (_, (td, _)) ->
830
                               not (Arrow.td_is_arrow td))) insts)) in
812
    let insts'' =
813
      List.(
814
        filter
815
          (fun l -> l <> [])
816
          (map (filter (fun (_, (td, _)) -> not (Arrow.td_is_arrow td))) insts))
817
    in
831 818
    let inputs = m.mstep.step_inputs in
832 819
    let outputs = m.mstep.step_outputs in
833
    pp_acsl_cut (fun fmt () ->
820
    pp_acsl_cut
821
      (fun fmt () ->
834 822
        if fst (get_stateless_status m) then
835
          fprintf fmt
836
            "%a@,%a@,%a@,%a"
837
            (pp_requires (pp_valid pp_var_decl)) outputs
838
            (pp_requires pp_separated') outputs
839
            (pp_assigns pp_ptr_decl) outputs
823
          fprintf fmt "%a@,%a@,%a@,%a"
824
            (pp_requires (pp_valid pp_var_decl))
825
            outputs
826
            (pp_requires pp_separated')
827
            outputs (pp_assigns pp_ptr_decl) outputs
840 828
            (pp_ensures (pp_transition_aux'' m))
841 829
            (name, inputs, [], outputs, "", "")
842 830
        else
843 831
          fprintf fmt
844 832
            "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
845
            (pp_requires (pp_valid pp_var_decl)) outputs
846
            (pp_requires pp_mem_valid') (name, self)
847
            (pp_requires (pp_separated self mem)) (insts', outputs)
833
            (pp_requires (pp_valid pp_var_decl))
834
            outputs
835
            (pp_requires pp_mem_valid')
836
            (name, self)
837
            (pp_requires (pp_separated self mem))
838
            (insts', outputs)
848 839
            (pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
849 840
            (name, mem, self)
850 841
            (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
851 842
            (name, mem, self)
852
            (pp_ensures (pp_transition_aux m (pp_old pp_ptr)
853
                           pp_ptr pp_var_decl pp_ptr_decl))
843
            (pp_ensures
844
               (pp_transition_aux m (pp_old pp_ptr) pp_ptr pp_var_decl
845
                  pp_ptr_decl))
854 846
            (name, inputs, [], outputs, mem, mem)
855 847
            (pp_assigns pp_ptr_decl) outputs
856
            (pp_assigns (pp_reg self)) m.mmemory
857
            (pp_assigns pp_reset_flag') [self]
858
            (pp_assigns (pp_memory self)) (memories insts')
859
            (pp_assigns (pp_register_chain self)) insts
860
            (pp_assigns (pp_reset_flag_chain self)) insts''
861
            (pp_assigns (pp_reg mem)) m.mmemory
862
            (pp_assigns pp_reset_flag') [mem]
863
            (pp_assigns (pp_memory ~indirect:false mem)) (memories insts')
864
            (pp_assigns (pp_register_chain ~indirect:false mem)) insts
865
            (pp_assigns (pp_reset_flag_chain ~indirect:false mem)) insts''
866
      )
848
            (pp_assigns (pp_reg self))
849
            m.mmemory
850
            (pp_assigns pp_reset_flag')
851
            [ self ]
852
            (pp_assigns (pp_memory self))
853
            (memories insts')
854
            (pp_assigns (pp_register_chain self))
855
            insts
856
            (pp_assigns (pp_reset_flag_chain self))
857
            insts''
858
            (pp_assigns (pp_reg mem))
859
            m.mmemory
860
            (pp_assigns pp_reset_flag')
861
            [ mem ]
862
            (pp_assigns (pp_memory ~indirect:false mem))
863
            (memories insts')
864
            (pp_assigns (pp_register_chain ~indirect:false mem))
865
            insts
866
            (pp_assigns (pp_reset_flag_chain ~indirect:false mem))
867
            insts'')
867 868
      fmt ()
868 869

  
869
  let pp_ghost_instr_code m self fmt instr = match instr.instr_desc with
870
  let pp_ghost_instr_code m self fmt instr =
871
    match instr.instr_desc with
870 872
    | MStateAssign (x, v) ->
871 873
      fprintf fmt "@,%a"
872
        (pp_acsl_line
873
           (pp_ghost
874
              (pp_assign m self (pp_c_var_read m))))
874
        (pp_acsl_line (pp_ghost (pp_assign m self (pp_c_var_read m))))
875 875
        (x, v)
876 876
    | MResetAssign b ->
877
      fprintf fmt "@,%a"
878
        (pp_acsl_line
879
           (pp_ghost
880
              (pp_reset_assign self)))
881
        b
877
      fprintf fmt "@,%a" (pp_acsl_line (pp_ghost (pp_reset_assign self))) b
882 878
    | MSetReset inst ->
883 879
      let td, _ = List.assoc inst m.minstances in
884 880
      if Arrow.td_is_arrow td then
885
         fprintf fmt "@,%a;"
886
           (pp_acsl_line
887
              (pp_ghost
888
                 (pp_arrow_reset_ghost self)))
889
           inst
890
    | _ -> ()
881
        fprintf fmt "@,%a;"
882
          (pp_acsl_line (pp_ghost (pp_arrow_reset_ghost self)))
883
          inst
884
    | _ ->
885
      ()
891 886

  
892 887
  let pp_step_instr_spec m self mem fmt instr =
893 888
    fprintf fmt "%a%a"
894
      (pp_ghost_instr_code m mem) instr
889
      (pp_ghost_instr_code m mem)
890
      instr
895 891
      (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut
896 892
         (pp_acsl_line' (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
897 893
      instr.instr_spec
......
899 895
  let pp_ghost_parameter mem fmt inst =
900 896
    GhostProto.pp_ghost_parameters ~cut:false fmt
901 897
      (match inst with
902
       | Some inst ->
903
         [inst, fun fmt inst -> fprintf fmt "&%a" pp_indirect' (mem, inst)]
904
       | None ->
905
         [mem, pp_print_string])
906

  
898
      | Some inst ->
899
        [ (inst, fun fmt inst -> fprintf fmt "&%a" pp_indirect' (mem, inst)) ]
900
      | None ->
901
        [ mem, pp_print_string ])
907 902
end
908 903

  
909 904
(**************************************************************************)
......
911 906
(**************************************************************************)
912 907

  
913 908
module MakefileMod = struct
914

  
915 909
  let other_targets fmt basename _nodename dependencies =
916 910
    fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
917 911
    (* EACSL version of library file . c *)
918 912
    fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
919 913
    fprintf fmt
920
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on e-acsl -print -ocode %s_eacsl.c@."
914
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on \
915
       e-acsl -print -ocode %s_eacsl.c@."
921 916
      basename basename;
922 917
    fprintf fmt "@.";
923 918
    fprintf fmt "@.";
924 919

  
925
    (* EACSL version of library file . c + main .c  *)
926
    fprintf fmt "%s_main_eacsl.c: %s.c %s.h %s_main.c@." basename basename basename basename;
927
    fprintf fmt "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c -then-on e-acsl -print -ocode %s_main_eacsl.i@."
920
    (* EACSL version of library file . c + main .c *)
921
    fprintf fmt "%s_main_eacsl.c: %s.c %s.h %s_main.c@." basename basename
922
      basename basename;
923
    fprintf fmt
924
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c \
925
       -then-on e-acsl -print -ocode %s_main_eacsl.i@."
928 926
      basename basename basename;
929 927
    (* Ugly hack to deal with eacsl bugs *)
930
    fprintf fmt "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c" basename basename;
928
    fprintf fmt "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c"
929
      basename basename;
931 930
    fprintf fmt "@.";
932 931
    fprintf fmt "@.";
933 932

  
934 933
    (* EACSL version of binary *)
935 934
    fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;
936
    fprintf fmt "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@." basename; (* compiling instrumented lib + main *)
935
    fprintf fmt "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@."
936
      basename;
937
    (* compiling instrumented lib + main *)
937 938
    C_backend_makefile.fprintf_dependencies fmt dependencies;
938
    fprintf fmt "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s %s_main_eacsl.o %a@."
939
    fprintf fmt
940
      "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s \
941
       %s_main_eacsl.o %a@."
939 942
      basename
940
      (Utils.fprintf_list ~sep:" " (fun fmt dep -> Format.fprintf fmt "%s.o" dep.name))
943
      (Utils.fprintf_list ~sep:" " (fun fmt dep ->
944
           Format.fprintf fmt "%s.o" dep.name))
941 945
      (C_backend_makefile.compiled_dependencies dependencies)
942 946
      ("${FRAMACEACSL}/e_acsl.c "
943
       ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
944
       ^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
947
     ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
948
     ^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
945 949
      basename
946 950
      (Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib))
947
      (C_backend_makefile.lib_dependencies dependencies)
948
    ;
951
      (C_backend_makefile.lib_dependencies dependencies);
949 952
    fprintf fmt "@."
950

  
951 953
end
952 954

  
953 955
(* Local Variables: *)

Also available in: Unified diff