Source file `clabels.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
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

(* -------------------------------------------------------------------------- *)
(* --- Normalized C-labels                                                --- *)
(* -------------------------------------------------------------------------- *)

open Cil_types

type c_label = string

let compare = String.compare
let equal (a:string) (b:string) = (a = b)

module T = struct type t = c_label let compare = compare end
module LabelMap = Datatype.String.Map
module LabelSet = Datatype.String.Set

let init = "wp:init"
let here = "wp:here"
let next = "wp:next"
let pre = "wp:pre"
let post = "wp:post"
let exit = "wp:exit"
let break = "wp:break"
let continue = "wp:continue"
let default = "wp:default"

let loopcurrent = "wp:loopcurrent"
let loopentry = "wp:loopentry"

let formal a = a

let pretty = Format.pp_print_string

let is_here h = (h = here)

let mem l lbl = List.mem l lbl

let case n = "wp:case" ^ Int64.to_string n
let stmt s = "wp:sid"  ^ string_of_int s.sid
let stmt_post s = "wp:sid:post:" ^ string_of_int s.sid
let loop_entry s = stmt s (* same point *)
let loop_current s = "wp:head" ^ string_of_int s.sid

let to_logic a = FormalLabel a
let of_logic = function
  | BuiltinLabel Here -> here
  | BuiltinLabel Init -> init
  | BuiltinLabel Pre -> pre
  | BuiltinLabel Post -> post
  | FormalLabel name -> name
  | BuiltinLabel Old -> "wp:old"
  | BuiltinLabel LoopCurrent -> loopcurrent
  | BuiltinLabel LoopEntry -> loopentry
  | StmtLabel s -> stmt !s

let is_post = function
  | BuiltinLabel Post -> true
  | FormalLabel a -> a = post || a = exit
  | _ -> false

let name = function FormalLabel a -> a | _ -> ""

let lookup labels a =
  try
    List.find (fun (l,_) -> name l = a) labels |> snd
  with Not_found ->
    Wp_parameters.fatal
      "Unbound label parameter '%s' in predicate or function call" a

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