package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file cfgAnnot.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Cil_types

(* -------------------------------------------------------------------------- *)
(* --- Smoke Tests                                                        --- *)
(* -------------------------------------------------------------------------- *)

let smoke kf ~id ?doomed ?unreachable () =
  WpPropId.mk_smoke kf ~id ?doomed ?unreachable () , Logic_const.pfalse

let get_unreachable kf stmt =
  WpPropId.mk_smoke kf ~id:"unreachabled" ~unreachable:stmt ()

(* -------------------------------------------------------------------------- *)
(* --- Memoization                                                        --- *)
(* -------------------------------------------------------------------------- *)

module CodeKey =
struct
  type t = kernel_function * stmt
  let compare (a:t) (b:t) = Stdlib.compare (snd a).sid (snd b).sid
  let pretty fmt (a:t) = Format.fprintf fmt "s%d" (snd a).sid
end

(* -------------------------------------------------------------------------- *)
(* --- Property Accessors : Behaviors                                     --- *)
(* -------------------------------------------------------------------------- *)

type behavior = {
  bhv_assumes: WpPropId.pred_info list ;
  bhv_requires: WpPropId.pred_info list ;
  bhv_smokes: WpPropId.pred_info list ;
  bhv_ensures: WpPropId.pred_info list ;
  bhv_exits: WpPropId.pred_info list ;
  bhv_post_assigns: WpPropId.assigns_full_info ;
  bhv_exit_assigns: WpPropId.assigns_full_info ;
}

let normalize_assumes h =
  let module L = NormAtLabels in
  L.preproc_annot L.labels_fct_pre h

let implies ?assumes p =
  match assumes with None -> p | Some h -> Logic_const.pimplies (h,p)

let filter ~goal ip =
  if goal
  then Logic_utils.verify_predicate ip.ip_content.tp_kind
  else Logic_utils.use_predicate ip.ip_content.tp_kind

let normalize_pre ~goal kf bhv ?assumes ip =
  if filter ~goal ip then
    let module L = NormAtLabels in
    let labels = L.labels_fct_pre in
    let id = WpPropId.mk_pre_id kf Kglobal bhv ip in
    let pre = ip.ip_content.tp_statement in
    let assumes = Option.map normalize_assumes assumes in
    let precond = L.preproc_annot labels pre in
    Some (id, implies ?assumes precond)
  else None

let normalize_post ~goal kf bhv tk ?assumes (itk,ip) =
  if tk = itk && filter ~goal ip then
    let module L = NormAtLabels in
    let at_pre e = Logic_const.pat (e, BuiltinLabel Pre) in
    let assumes = Option.map (fun p -> normalize_assumes @@ at_pre p) assumes in
    let labels = L.labels_fct_post ~exit:(tk=Exits) in
    let id = WpPropId.mk_post_id kf Kglobal bhv (tk,ip) in
    let post = L.preproc_annot labels ip.ip_content.tp_statement in
    Some (id , implies ?assumes post)
  else None

let normalize_decreases (d, li) =
  let module L = NormAtLabels in
  let at_pre e = Logic_const.tat (e, BuiltinLabel Pre) in
  let labels = L.labels_fct_pre in
  (at_pre @@ L.preproc_term labels d, li)

let normalize_froms tk froms =
  let module L = NormAtLabels in
  let labels = L.labels_fct_assigns ~exit:(tk=Exits) in
  L.preproc_assigns labels froms

let normalize_fct_assigns kf ~exits bhv = function
  | WritesAny ->
    WpPropId.empty_assigns_info, WpPropId.empty_assigns_info
  | Writes froms ->
    let make tk =
      match WpPropId.mk_fct_assigns_id kf exits bhv tk froms with
      | None -> WpPropId.empty_assigns_info
      | Some id ->
        let assigns = normalize_froms tk froms in
        let desc = WpPropId.mk_kf_assigns_desc assigns in
        WpPropId.mk_assigns_info id desc
    in
    make Normal,
    if exits then make Exits else WpPropId.empty_assigns_info

let get_behavior_goals kf ?(smoking=false) ?(exits=false) bhv =
  let pre_cond = normalize_pre ~goal:false kf bhv in
  let post_cond = normalize_post ~goal:true kf bhv in
  let p_asgn, e_asgn = normalize_fct_assigns kf ~exits bhv bhv.b_assigns in
  let smokes =
    let do_assumes =
      Wp_parameters.SmokeDeadassumes.get() && bhv.b_assumes <> [] in
    if smoking && (bhv.b_requires <> [] || do_assumes) then
      let bname =
        if Cil.is_default_behavior bhv then "default" else bhv.b_name in
      let id, doomed =
        if bhv.b_requires <> []
        then
          bname ^ "_requires",
          Property.ip_requires_of_behavior kf Kglobal bhv
        else
          bname ^ "_assumes",
          Property.ip_assumes_of_behavior kf Kglobal bhv
      in
      [smoke kf ~id ~doomed ()]
    else []
  in
  {
    bhv_assumes = List.filter_map pre_cond bhv.b_assumes;
    bhv_requires = List.filter_map pre_cond bhv.b_requires;
    bhv_ensures = List.filter_map (post_cond Normal) bhv.b_post_cond ;
    bhv_exits = List.filter_map (post_cond Exits) bhv.b_post_cond ;
    bhv_post_assigns = p_asgn ;
    bhv_exit_assigns = e_asgn ;
    bhv_smokes = smokes;
  }

(* -------------------------------------------------------------------------- *)
(* --- Side Behavior Requires                                             --- *)
(* -------------------------------------------------------------------------- *)

let get_requires ~goal kf bhv =
  List.filter_map (normalize_pre ~goal kf bhv) bhv.b_requires

let get_preconditions ~goal kf =
  let module L = NormAtLabels in
  let mk_pre = L.preproc_annot L.labels_fct_pre in
  List.map
    (fun bhv ->
       let p = Ast_info.behavior_precondition ~goal bhv in
       let ip = Logic_const.new_predicate p in
       WpPropId.mk_pre_id kf Kglobal bhv ip,  mk_pre p
    ) (Annotations.behaviors kf)

let get_complete_behaviors kf =
  let spec = Annotations.funspec kf in
  let module L = NormAtLabels in
  List.map
    (fun bs ->
       WpPropId.mk_compl_bhv_id (kf,Kglobal,[],bs) ,
       L.preproc_annot L.labels_fct_pre @@ Ast_info.complete_behaviors spec bs
    ) spec.spec_complete_behaviors

let get_disjoint_behaviors kf =
  let spec = Annotations.funspec kf in
  let module L = NormAtLabels in
  List.map
    (fun bs ->
       WpPropId.mk_disj_bhv_id (kf,Kglobal,[],bs) ,
       L.preproc_annot L.labels_fct_pre @@ Ast_info.disjoint_behaviors spec bs
    ) spec.spec_disjoint_behaviors

let normalize_terminates p =
  let module L = NormAtLabels in
  L.preproc_annot L.labels_fct_pre @@
  Logic_const.pat (p.ip_content.tp_statement, BuiltinLabel Pre)

let get_terminates_goal kf =
  let make_pred_info p =
    WpPropId.mk_terminates_id kf Kglobal p, normalize_terminates p in
  Option.map make_pred_info @@ Annotations.terminates kf

let get_terminates_hyp kf =
  match get_terminates_goal kf with
  | None -> true, Logic_const.pfalse
  | Some (_, p) -> false, p

let check_variant_relation = function
  | (_, None) -> ()
  | ({ term_loc }, Some rel) ->
    Wp_parameters.hypothesis
      ~source:(fst term_loc) ~once:true
      "'%a' relation must be well-founded" Cil_printer.pp_logic_info rel

let get_decreases_goal kf =
  let defined t = WpPropId.mk_decrease_id kf Kglobal t, normalize_decreases t in
  match Annotations.decreases kf with
  | None -> None
  | Some v -> check_variant_relation v ; Some (defined v)

let get_decreases_hyp kf =
  Annotations.decreases kf

(* -------------------------------------------------------------------------- *)
(* --- Contracts                                                          --- *)
(* -------------------------------------------------------------------------- *)

type contract = {
  contract_cond : WpPropId.pred_info list ;
  contract_hpre : WpPropId.pred_info list ;
  contract_post : WpPropId.pred_info list ;
  contract_exit : WpPropId.pred_info list ;
  contract_smoke : WpPropId.pred_info list ;
  contract_assigns : Cil_types.assigns ;
  contract_terminates : bool * Cil_types.predicate ;
  contract_decreases : Cil_types.variant option ;
}

let default_assigns behaviors =
  try (List.find Cil.is_default_behavior behaviors).b_assigns
  with Not_found -> WritesAny

let unguarded_behavior_assigns behaviors =
  let unguarded_assigns b = b.b_assumes = [] && b.b_assigns <> WritesAny in
  try (List.find unguarded_assigns behaviors).b_assigns
  with Not_found -> WritesAny

let assigns_of_complete behaviors complete =
  let in_complete b = List.exists (String.equal b.b_name) complete in
  let behaviors = List.filter in_complete behaviors in
  let concat a bhv = Logic_utils.concat_assigns a bhv.b_assigns in
  List.fold_left concat (Writes []) behaviors

let complete_assigns behaviors completes =
  let exception Found of assigns in
  let find_complete complete =
    match assigns_of_complete behaviors complete with
    | WritesAny -> ()
    | assigns -> raise (Found assigns)
  in
  try List.iter find_complete completes ; WritesAny
  with Found assigns -> assigns

let assigns_upper_bound behaviors completes =
  match default_assigns behaviors with
  | Writes _ as assigns -> assigns
  | WritesAny ->
    match unguarded_behavior_assigns behaviors with
    | Writes _ as assigns ->
      Wp_parameters.warning ~once:true ~current:true
        "No default assigns clause, using unguarded behavior assigns" ;
      assigns
    | WritesAny ->
      match complete_assigns behaviors completes with
      | Writes _ as assigns ->
        Wp_parameters.warning ~once:true ~current:true
          "No default assigns clause, using complete behaviors assigns" ;
        assigns
      | WritesAny ->
        (* We don't warn here, WritesAny have special treatment in CfgCalculus*)
        WritesAny

(* -------------------------------------------------------------------------- *)
(* --- Call Contracts                                                     --- *)
(* -------------------------------------------------------------------------- *)

(*TODO: put it in Status_by_call ? *)
module AllPrecondStatus =
  State_builder.Hashtbl(Kernel_function.Hashtbl)(Datatype.Unit)
    (struct
      let name = "Wp.CfgAnnot.AllPrecondStatus"
      let dependencies = [Ast.self]
      let size = 32
    end)

let setup_preconditions kf =
  if not (AllPrecondStatus.mem kf) then
    begin
      AllPrecondStatus.add kf () ;
      Statuses_by_call.setup_all_preconditions_proxies kf ;
    end

let get_precond_at kf stmt (id,p) =
  let pi = WpPropId.property_of_id id in
  let pi_at = Statuses_by_call.precondition_at_call kf pi stmt in
  let id_at = WpPropId.mk_call_pre_id kf stmt pi pi_at in
  id_at , p

module CallContract = WpContext.StaticGenerator(Kernel_function)
    (struct
      type key = kernel_function
      type data = contract
      let name = "Wp.CfgAnnot.CallContract"
      let compile kf =
        let wcond : WpPropId.pred_info list ref = ref [] in
        let whpre : WpPropId.pred_info list ref = ref [] in
        let wpost : WpPropId.pred_info list ref = ref [] in
        let wexit : WpPropId.pred_info list ref = ref [] in
        let add w f x = match f x with Some y -> w := y :: !w | None -> () in
        let behaviors = Annotations.behaviors kf in
        let completes = Annotations.complete kf in
        setup_preconditions kf ;
        List.iter
          begin fun bhv ->
            (* Normalization of assumes is specific to each case *)
            let assumes = Ast_info.behavior_assumes bhv in
            let mk_cond = normalize_pre ~goal:true kf bhv ~assumes in
            let mk_hpre = normalize_pre ~goal:false kf bhv ~assumes in
            let mk_post = normalize_post ~goal:false kf bhv ~assumes in
            List.iter (add wcond @@ mk_cond) bhv.b_requires ;
            List.iter (add whpre @@ mk_hpre) bhv.b_requires ;
            List.iter (add wpost @@ mk_post Normal) bhv.b_post_cond ;
            List.iter (add wexit @@ mk_post Exits) bhv.b_post_cond ;
          end behaviors ;
        let assigns = match assigns_upper_bound behaviors completes with
          | WritesAny -> WritesAny
          | Writes froms -> Writes (normalize_froms Normal froms)
        in
        let terminates = get_terminates_hyp kf in
        let decreases = Option.map normalize_decreases @@ get_decreases_hyp kf in
        {
          contract_cond = List.rev !wcond ;
          contract_hpre = List.rev !whpre ;
          contract_post = List.rev !wpost ;
          contract_exit = List.rev !wexit ;
          contract_smoke = [] ;
          contract_assigns = assigns ;
          contract_terminates = terminates ;
          contract_decreases = decreases ;
        }
    end)

let get_call_contract ?smoking kf stmt =
  let cc = CallContract.get kf in
  let preconds = List.map (get_precond_at kf stmt) cc.contract_cond in
  match smoking with
  | None ->
    { cc with contract_cond = preconds }
  | Some s ->
    let g = smoke kf ~id:"dead_call" ~unreachable:s () in
    { cc with contract_cond = preconds ; contract_smoke = [ g ] }

(* -------------------------------------------------------------------------- *)
(* --- Assembly Code                                                      --- *)
(* -------------------------------------------------------------------------- *)

let is_assembly stmt =
  match stmt.skind with
  | Instr (Asm _) -> true
  | _ -> false

let get_stmt_assigns kf stmt =
  let asgn =
    Annotations.fold_code_annot
      begin fun _emitter ca l ->
        match ca.annot_content with
        | AStmtSpec(fors,s) ->
          List.fold_left
            (fun l bhv ->
               match bhv.b_assigns with
               | WritesAny -> l
               | Writes froms ->
                 let module L = NormAtLabels in
                 let labels = L.labels_stmt_assigns ~kf stmt in
                 match
                   WpPropId.mk_stmt_assigns_id kf stmt fors bhv froms
                 with
                 | None -> l
                 | Some id ->
                   let froms = L.preproc_assigns labels froms in
                   let desc = WpPropId.mk_stmt_assigns_desc stmt froms in
                   WpPropId.mk_assigns_info id desc :: l
            ) l s.spec_behavior
        | _ -> l
      end stmt []
  in if asgn = [] then [WpPropId.mk_stmt_any_assigns_info stmt] else asgn

(* -------------------------------------------------------------------------- *)
(* --- Code Assertions                                                    --- *)
(* -------------------------------------------------------------------------- *)

type code_assertion = {
  code_admitted: WpPropId.pred_info option ;
  code_verified: WpPropId.pred_info option ;
}

(* Note: collected in REVERSE order *)
module CodeAssertions = WpContext.StaticGenerator(CodeKey)
    (struct
      type key = CodeKey.t
      type data = code_assertion list
      let name = "Wp.CfgAnnot.CodeAssertions"
      let compile (kf,stmt) =
        let labels = NormAtLabels.labels_assert ~kf stmt in
        let normalize_pred p = NormAtLabels.preproc_annot labels p in
        let all_annot = (* ensures that the order is the one displayed in GUI *)
          List.sort
            Cil_datatype.Code_annotation.compare
            (Annotations.code_annot stmt)
        in
        List.fold_left
          begin fun l ca ->
            match ca.annot_content with
            | AStmtSpec _ when not @@ is_assembly stmt ->
              let source = fst (Cil_datatype.Stmt.loc stmt) in
              Wp_parameters.warning ~once:true ~source
                "Statement specifications not yet supported (skipped)." ; l
            | AInvariant(_,false,_) ->
              let source = fst (Cil_datatype.Stmt.loc stmt) in
              Wp_parameters.warning ~once:true ~source
                "Generalized invariant not yet supported (skipped)." ; l
            | AAssert(_,a) ->
              let p =
                WpPropId.mk_assert_id kf stmt ca ,
                normalize_pred a.tp_statement in
              let admit = Logic_utils.use_predicate a.tp_kind in
              let verif = Logic_utils.verify_predicate a.tp_kind in
              let use flag p = if flag then Some p else None in
              {
                code_admitted = use admit p ;
                code_verified = use verif p ;
              } :: l
            | _ -> l
          end [] all_annot
    end)

let get_code_assertions ?(smoking=false) kf stmt =
  let ca = CodeAssertions.get (kf,stmt) in
  (* Make sure that smoke tests are in the end so that it can see surely false
     assertions associated to this statement, in particular RTE assertions.   *)
  List.rev @@
  if smoking then
    let s = smoke kf ~id:"dead_code" ~unreachable:stmt () in
    { code_admitted = None ; code_verified = Some s } :: ca
  else ca

(* -------------------------------------------------------------------------- *)
(* --- Loop Invariants                                                    --- *)
(* -------------------------------------------------------------------------- *)

let mk_variant_properties kf s ca v =
  let vpos_id = WpPropId.mk_var_pos_id kf s ca in
  let vdecr_id = WpPropId.mk_var_decr_id kf s ca in
  let loc = v.term_loc in
  let lcurr = Clabels.to_logic (Clabels.loop_current s) in
  let vcurr = Logic_const.tat ~loc (v, lcurr) in
  let zero = Cil.lzero ~loc () in
  let vpos = Logic_const.prel ~loc (Rle, zero, vcurr) in
  let vdecr = Logic_const.prel ~loc (Rlt, v, vcurr) in
  (vpos_id, vpos), (vdecr_id, vdecr)

let mk_variant_relation_property kf s ca v li =
  check_variant_relation (v, Some li) ;
  let vid = WpPropId.mk_var_id kf s ca in
  let loc = v.term_loc in
  let lcurr = Clabels.to_logic (Clabels.loop_current s) in
  let vcurr = Logic_const.tat ~loc (v, lcurr) in
  let variant = Logic_const.papp ~loc (li,[],[vcurr ; v]) in
  (vid, variant)

type loop_hypothesis =
  | NoHyp
  | Check of WpPropId.prop_id
  | Always of WpPropId.prop_id

type loop_invariant = {
  loop_hyp : loop_hypothesis ;
  loop_est : WpPropId.prop_id option ;
  loop_ind : WpPropId.prop_id option ;
  loop_pred : Cil_types.predicate ;
}

type loop_contract = {
  loop_terminates: predicate option;
  loop_invariants : loop_invariant list ;
  (* to be proved after loop invariants *)
  loop_smoke: WpPropId.pred_info list;
  (* assigned by loop body *)
  loop_assigns: WpPropId.assigns_full_info list;
}

let default_assigns stmt l =
  { l with
    loop_assigns =
      if l.loop_assigns <> [] then l.loop_assigns
      else [WpPropId.mk_loop_any_assigns_info stmt] }

module LoopContract = WpContext.StaticGenerator(CodeKey)
    (struct
      type key = CodeKey.t
      type data = loop_contract
      let name = "Wp.CfgAnnot.LoopContract"
      let compile (kf,stmt) =
        let labels = NormAtLabels.labels_loop stmt in
        let normalize_pred p = NormAtLabels.preproc_annot labels p in
        let normalize_annot (i,p) = i, normalize_pred p in
        let normalize_assigns w = NormAtLabels.preproc_assigns labels w in
        let intro_terminates_variant ~loc (pid, v) =
          pid,
          let t = snd @@ get_terminates_hyp kf in
          if Wp_parameters.TerminatesVariantHyp.get () then begin
            if Logic_utils.is_same_predicate t Logic_const.pfalse then
              Wp_parameters.warning
                ~source:(fst loc) ~once:true
                "Loop variant is always trivially verified \
                 (terminates \\false)" ;
            Logic_const.pimplies (t, v)
          end else v
        in
        let variant_as_inv ~loc (i, p) =
          let i, p = intro_terminates_variant ~loc @@ normalize_annot (i, p) in
          { loop_pred = p ;
            loop_hyp = NoHyp ; loop_est = None ; loop_ind = Some i }
        in
        let all_annot = (* ensures that the order is the one displayed in GUI *)
          List.rev @@ List.sort
            Cil_datatype.Code_annotation.compare
            (Annotations.code_annot stmt)
        in
        default_assigns stmt @@
        List.fold_left
          begin fun l ca ->
            match ca.annot_content with
            | AInvariant(_,true,inv) ->
              let g_hyp = WpPropId.mk_inv_hyp_id kf stmt ca in
              let g_est, g_ind = WpPropId.mk_loop_inv kf stmt ca in
              let admit = Logic_utils.use_predicate inv.tp_kind in
              let verif = Logic_utils.verify_predicate inv.tp_kind in
              let loop_hyp = if admit then Always g_hyp else Check g_hyp in
              let use flag id = if flag then Some id else None in
              let inv =
                { loop_pred = normalize_pred inv.tp_statement ;
                  loop_hyp ;
                  loop_est = use verif g_est ;
                  loop_ind = use verif g_ind ; }
              in
              { l with
                loop_invariants  = inv :: l.loop_invariants ; }
            | AVariant(term, None) ->
              let vpos , vdec = mk_variant_properties kf stmt ca term in
              let vpos = variant_as_inv ~loc:term.term_loc vpos in
              let vdec = variant_as_inv ~loc:term.term_loc vdec in
              { l with loop_terminates = None ;
                       loop_invariants = vdec :: vpos :: l.loop_invariants }
            | AVariant(term, Some rel) ->
              let vrel = mk_variant_relation_property kf stmt ca term rel in
              let vrel = variant_as_inv ~loc:term.term_loc vrel in
              { l with loop_terminates = None ;
                       loop_invariants = vrel :: l.loop_invariants }
            | AAssigns(_,WritesAny) ->
              let asgn = WpPropId.mk_loop_any_assigns_info stmt in
              { l with loop_assigns = asgn :: l.loop_assigns }
            | AAssigns(_,Writes w) ->
              begin match WpPropId.mk_loop_assigns_id kf stmt ca w with
                | None -> l (* shall not occur *)
                | Some id ->
                  let w = normalize_assigns w in
                  let a = WpPropId.mk_loop_assigns_desc stmt w in
                  let asgn = WpPropId.mk_assigns_info id a in
                  { l with loop_assigns = asgn :: l.loop_assigns }
              end
            | _ -> l
          end
          { loop_terminates = Some Logic_const.pfalse ;
            loop_invariants = [] ;
            loop_smoke = [] ;
            loop_assigns = [] ;
          }
          all_annot
    end)

let get_loop_contract ?(smoking=false) ?terminates kf stmt =
  (* Loop Contract *)
  let lc = LoopContract.get (kf,stmt) in
  (* Loop Smoking *)
  let lc =
    if smoking && not (WpReached.is_dead_code stmt) then
      let g = smoke kf ~id:"dead_loop" ~unreachable:stmt () in
      { lc with loop_smoke = g :: lc.loop_smoke }
    else lc
  in
  (* Loop Termination *)
  match lc.loop_terminates, terminates with
  | None, _ -> lc
  | Some _, None -> { lc with loop_terminates = None }
  | Some loop_terminates, Some terminates ->
    let prop = Logic_const.pimplies(terminates, loop_terminates) in
    { lc with loop_terminates = Some prop }

(* -------------------------------------------------------------------------- *)
(* --- Clear Tablesnts                                                    --- *)
(* -------------------------------------------------------------------------- *)

let clear () =
  CallContract.clear () ;
  LoopContract.clear () ;
  CodeAssertions.clear ()

(* -------------------------------------------------------------------------- *)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct