Project

General

Profile

Revision 17e1d0f4

View differences:

TODO.org
134 134
** Development
135 135
*** Done
136 136
*** To be done
137
**** Court terme
138

  
139
- repartir la branche acsl2018 qui contient la normalisation des eexpr
140
  - le refaire compiler
141
  - merger avec unstable 
142
- transformer cette normalisation pour partager les definitions locales de
143
  variables dans le noeud de spec, aka contract
144
- retirer le parser Kind21 et revenir à celui de lustrec
145
- (CG) etendre la syntaxe pour coller à la definition donnée ci-dessus
146
  - lexeur/parseur lustreSpec + document latex de grammaire
147

  
148
**** Apres
149
- developper dans les backends
150
  - C
151
  - EMF
152
  - LustreV
137 153

  
138 154
* TODO refactoring + doc
139 155
- separate lustre types from machine types in different files
src/_tags.in
16 16
"tools/stateflow/semantics": include
17 17
"tools/stateflow/models": include
18 18
"tools/stateflow/json-parser": include
19
"cocospec": include
20 19

  
21 20
# svn
22 21
<**/.svn>: -traverse
src/cocospec/kindIdent.ml
1
(* This file is part of the Kind 2 model checker.
2

  
3
   Copyright (c) 2014 by the Board of Trustees of the University of Iowa
4

  
5
   Licensed under the Apache License, Version 2.0 (the "License"); you
6
   may not use this file except in compliance with the License.  You
7
   may obtain a copy of the License at
8

  
9
   http://www.apache.org/licenses/LICENSE-2.0 
10

  
11
   Unless required by applicable law or agreed to in writing, software
12
   distributed under the License is distributed on an "AS IS" BASIS,
13
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
14
   implied. See the License for the specific language governing
15
   permissions and limitations under the License. 
16

  
17
*)
18

  
19
open KindLib
20

  
21

  
22
(* TODO: 
23

  
24
   - Hashccons identifiers and use for StateVar, UfSymbol etc. 
25

  
26
   - Hide implementation and provide smart constructors that fail if
27
     identifier was previously defined
28

  
29
   - Allow several namespaces to avoid spurious name clashes
30

  
31
   - List reserved identifiers per namespace and fail if reserved
32
     identifier is created
33

  
34
   - Use tag of identifier as short name instead of full string when
35
     passing to SMT solver etc.
36

  
37
*)
38

  
39
(* Namespace to avoid clashes between reserved and user identifiers *)
40
type namespace =
41

  
42
  (* Reserved identifier *)
43
  | ReservedIdentifier
44

  
45
  (* Identifier in user input *)
46
  | UserIdentifier
47

  
48
module Ident = struct
49

  
50
  (* Identifier with namespace *)
51
  (* type t = namespace * string *)
52
  type t = string
53
    
54
  (* Equality on identifiers *)
55
  let equal = String.equal
56
              
57
  (* Total order on identifiers *)
58
  let compare = String.compare 
59

  
60
end
61

  
62
include Ident
63

  
64
module IdentSet = Set.Make (Ident)
65

  
66
module IdentMap = Map.Make (Ident)
67

  
68

  
69
let pp_print_ident ppf i = Format.fprintf ppf "%s" i
70

  
71
(* Construct an identifier from a string
72

  
73
   Simply return the string for now, later do some smarter things. *)
74
let of_string s = s
75

  
76
let to_string = string_of_t pp_print_ident 
77

  
78
(* 
79
   Local Variables:
80
   compile-command: "make -C .. -k"
81
   indent-tabs-mode: nil
82
   End: 
83
*)
src/cocospec/kindIdent.mli
1
(* This file is part of the Kind 2 model checker.
2

  
3
   Copyright (c) 2014 by the Board of Trustees of the University of Iowa
4

  
5
   Licensed under the Apache License, Version 2.0 (the "License"); you
6
   may not use this file except in compliance with the License.  You
7
   may obtain a copy of the License at
8

  
9
   http://www.apache.org/licenses/LICENSE-2.0 
10

  
11
   Unless required by applicable law or agreed to in writing, software
12
   distributed under the License is distributed on an "AS IS" BASIS,
13
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
14
   implied. See the License for the specific language governing
15
   permissions and limitations under the License. 
16

  
17
*)
18

  
19
(** Managing of identifier to avoid clashes
20

  
21
    @author Christoph Sticksel *)
22

  
23
(** Identifier 
24

  
25
    This type will become private later *)
26
type t = string
27

  
28
(** Equality of identifiers *)
29
val equal : t -> t -> bool
30

  
31
(** Total order of identifiers *)
32
val compare : t -> t -> int
33

  
34
(** Set of identifiers *)
35
module IdentSet : Set.S with type elt = t
36

  
37
(** Map of identifiers *)
38
module IdentMap : Map.S with type key = t
39

  
40
(** Pretty-print an identifier *)
41
val pp_print_ident : Format.formatter -> t -> unit
42

  
43
(** Construct an identifier from a string *)
44
val of_string : string -> t
45

  
46
(** Return a string representation of an identifier x*)
47
val to_string : t -> string 
48

  
49
(* 
50
   Local Variables:
51
   compile-command: "make -C .. -k"
52
   indent-tabs-mode: nil
53
   End: 
54
*)
src/cocospec/kindLib.ml
1
(* This file is part of the Kind 2 model checker.
2

  
3
   Copyright (c) 2015 by the Board of Trustees of the University of Iowa
4

  
5
   Licensed under the Apache License, Version 2.0 (the "License"); you
6
   may not use this file except in compliance with the License.  You
7
   may obtain a copy of the License at
8

  
9
   http://www.apache.org/licenses/LICENSE-2.0 
10

  
11
   Unless required by applicable law or agreed to in writing, software
12
   distributed under the License is distributed on an "AS IS" BASIS,
13
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
14
   implied. See the License for the specific language governing
15
   permissions and limitations under the License. 
16

  
17
*)
18

  
19
open Format
20

  
21
(* ********************************************************************** *)
22
(* Helper functions                                                       *)
23
(* ********************************************************************** *)
24

  
25
(* Identity function. *)
26
let identity anything = anything
27

  
28
(* Prints the first argument and returns the second. *)
29
let print_pass s whatever =
30
  printf "%s@." s ;
31
  whatever
32

  
33
(* Returns true when given unit. *)
34
let true_of_unit () = true
35

  
36
(* Returns false when given unit. *)
37
let false_of_unit () = false
38

  
39
(* Returns None when given unit. *)
40
let none_of_unit () = None
41

  
42
(* Returns true *)
43
let true_of_any _ = true
44

  
45
(* Returns false s*)
46
let false_of_any _ = false
47

  
48
(* Creates a directory if it does not already exist. *)
49
let mk_dir dir =
50
  try Unix.mkdir dir 0o740 with Unix.Unix_error(Unix.EEXIST, _, _) -> ()
51

  
52

  
53
(* ********************************************************************** *)
54
(* Arithmetic functions                                                   *)
55
(* ********************************************************************** *)
56

  
57
(* Compute [m * h + i] and make sure that the result does not overflow
58
   to a negtive number *)
59
let safe_hash_interleave h m i = abs(i + (m * h) mod max_int)
60

  
61
(* ********************************************************************** *)
62
(* List functions                                                         *)
63
(* ********************************************************************** *)
64

  
65
(* Add element to the head of the list if the option value is not [None] *)
66
let ( @:: ) = 
67
    function
68
    | None -> (function l -> l)
69
    | Some e -> (function l -> e :: l)
70

  
71

  
72
(* Creates a size-n list equal to [f 0; f 1; ... ; f (n-1)] *)
73
let list_init f n =
74
  if n = 0 then [] else
75
    let rec init_aux i =
76
      if i = n-1 then
77
        [f i]
78
      else
79
        (f i) :: (init_aux (i+1))
80
    in
81
    init_aux 0
82

  
83
(* Returns the maximum element of a non-empty list *)
84
let list_max l =
85
  assert (List.length l > 0);
86
  let rec list_max_aux l acc =
87
    match l with
88
    | [] ->
89
       acc
90
    | hd :: tl ->
91
       list_max_aux tl (max hd acc)
92
  in
93
  list_max_aux l (List.hd l)
94
             
95
(* Return the index of the first element that satisfies the predicate [p] *)
96
let list_index p = 
97
  let rec list_index p i = function
98
    | [] -> raise Not_found
99
    | x :: l -> if p x then i else list_index p (succ i) l
100
  in
101
  list_index p 0 
102

  
103

  
104
(* [list_indexes l1 l2] returns the indexes in list [l2] of elements in
105
   list [l1] *)
106
let rec list_indexes' accum pos l = function 
107

  
108
  | [] -> List.rev accum
109

  
110
  | h :: tl -> 
111

  
112
    if List.mem h l then 
113
      list_indexes' (pos :: accum) (succ pos) l tl
114
    else
115
      list_indexes' accum (succ pos) l tl
116

  
117

  
118
let list_indexes l1 l2 = list_indexes' [] 0 l1 l2
119

  
120

  
121

  
122

  
123
(* [list_filter_nth l [p1; p2; ...]] returns the elements [l] at positions [p1], [p2] etc. *)
124
let rec list_filter_nth' current_pos accum = 
125

  
126
  function 
127

  
128
    | [] -> (function _ -> List.rev accum)
129

  
130
    | h :: list_tl -> 
131

  
132
      (function 
133
        | next_pos :: positions_tl when current_pos = next_pos -> 
134

  
135

  
136
          (match positions_tl with
137

  
138
            | next_pos' :: _ when next_pos >= next_pos' -> 
139
              
140
              raise 
141
                (Invalid_argument
142
                   "list_filter_nth: list of position is not sorted")
143
                
144
            | _ -> 
145
              
146
              list_filter_nth' 
147
                (succ current_pos) 
148
                (h :: accum) 
149
                list_tl 
150
                positions_tl)
151
      
152
        | positions -> 
153
          
154
          list_filter_nth' (succ current_pos) accum list_tl positions)
155

  
156

  
157
let list_filter_nth l p = list_filter_nth' 0 [] l p
158

  
159

  
160
let list_extract_nth l i =
161
  let rec aux acc l i = match i, l with
162
    | 0, x :: r -> x, List.rev_append acc r
163
    | i, x :: r when i > 0 -> aux (x :: acc) r (i - 1) 
164
    | _ -> raise (Invalid_argument "list_extract_nth")
165
  in
166
  aux [] l i
167

  
168

  
169
(* [chain_list \[e1; e2; ...\]] is \[\[e1; e2\]; \[e2; e3\]; ... \]]*)
170
let chain_list = function 
171

  
172
  | [] 
173
  | _ :: [] -> invalid_arg "chain_list"
174

  
175
  | h :: tl -> 
176
    
177
    let rec chain_list (accum, last) curr = ([last; curr] :: accum, curr) in
178
    List.rev (fst (List.fold_left chain_list ([], h) tl))
179

  
180

  
181

  
182
(* Return a list containing all values in the first list that are not
183
    in the second list *)
184
let list_subtract l1 l2 = 
185
  List.filter
186
    (function e -> not (List.mem e l2))
187
    l1
188

  
189

  
190
(* From a sorted list return a list with physical duplicates removed *)
191
let list_uniq l = 
192
  let rec list_uniq accum = function 
193
    | [] -> List.rev accum
194
    | h1 :: tl -> 
195
      match accum with 
196
        | [] -> list_uniq [h1] tl
197
        | h2 :: _ -> 
198
          if h1 == h2 then list_uniq accum tl else list_uniq (h1 :: accum) tl
199
  in
200

  
201
  list_uniq [] l
202

  
203

  
204
(* Merge two sorted lists without physical duplicates to a sorted list without
205
   physical duplicates *)
206
let list_merge_uniq cmp l1 l2 = 
207
  
208
  let rec list_merge_uniq cmp accum l1 l2 = match l1, l2 with
209

  
210
    (* One of the lists is empty: reverse accumulator, append
211
       other list and return *)
212
    | [], l 
213
    | l, [] -> List.rev_append accum l
214

  
215
    (* First and second head elements are physically equal: remove
216
       head element from second list *)
217
    | h1 :: _, h2 :: tl when h1 == h2 -> list_merge_uniq cmp accum l1 tl
218

  
219
    (* First head element is smaller than second: add first head
220
       element to accumulator *)
221
    | h1 :: tl, h2 :: _ when cmp h1 h2 < 0 -> 
222
      list_merge_uniq cmp (h1 :: accum) tl l2
223

  
224
    (* First head element is greater than second: add second head
225
       element to accumulator *)
226
    | h1 :: _, h2 :: tl when cmp h1 h2 > 0 -> 
227
      list_merge_uniq cmp (h2 :: accum) l1 tl
228

  
229
    (* Head elements are structurally but not physically equal: keep
230
       both in original order *)
231
    | h1 :: tl1, h2 :: tl2 -> 
232
      list_merge_uniq cmp (h2 :: h1 :: accum) tl1 tl2
233
  in
234

  
235
  list_merge_uniq cmp [] l1 l2
236

  
237

  
238
(* From two sorted lists without physical duplicates return a sorted
239
   list without physical duplicates containing elements in both lists *)
240
let list_inter_uniq cmp l1 l2 = 
241

  
242
  let rec list_inter_uniq cmp accum l1 l2 = match l1, l2 with 
243

  
244
    (* One of the lists is empty: reverse accumulator and return *)
245
    | [], l
246
    | l, [] -> List.rev accum
247

  
248
    (* First and second head elements are physically equal: add first
249
       head element to accumulator *)
250
    | h1 :: tl1, h2 :: tl2 when h1 == h2 -> 
251
      list_inter_uniq cmp (h1 :: accum) tl1 tl2
252

  
253
    (* First head element is smaller than second: remove first head
254
       element from list *)
255
    | h1 :: tl, h2 :: _ when cmp h1 h2 < 0 -> 
256
      list_inter_uniq cmp accum tl l2
257

  
258
    (* First head element is greater than or structurally but not
259
       physically equal to second: remove second head element from
260
       list *)
261
    | h1 :: _, h2 :: tl ->
262
      list_inter_uniq cmp accum l1 tl
263
  in
264

  
265
  list_inter_uniq cmp [] l1 l2
266

  
267

  
268
(* From two sorted lists without physical duplicates return a sorted
269
   list without physical duplicates containing elements in the first
270
   but not in the second list *)
271
let list_diff_uniq cmp l1 l2 = 
272

  
273
  let rec list_diff_uniq cmp accum l1 l2 = match l1, l2 with 
274

  
275
    (* First list is empty: reverse accumulator and return *)
276
    | [], l -> List.rev accum
277

  
278
    (* Second list is empty: reverse accumulator, append first list
279
       and return *)
280
    | l, [] -> List.rev_append accum l
281

  
282
    (* First and second head elements are physically equal: remove
283
       both head elements *)
284
    | h1 :: tl1, h2 :: tl2 when h1 == h2 -> 
285
      list_diff_uniq cmp accum tl1 tl2
286

  
287
    (* First head element is smaller than second: add first head
288
       element to accumulator *)
289
    | h1 :: tl, h2 :: _ when cmp h1 h2 < 0 -> 
290
      list_diff_uniq cmp (h1 :: accum) tl l2
291

  
292
    (* First head element is greater than second: remove first head
293
       element from list *)
294
    | h1 :: _, h2 :: tl ->
295
      list_diff_uniq cmp accum l1 tl
296
  in
297

  
298
  list_diff_uniq cmp [] l1 l2
299

  
300

  
301
(* For two sorted lists without physical duplicates return true if the
302
   first list contains a physically equal element for each element in
303
   the second list *)
304
let rec list_subset_uniq cmp l1 l2 = match l1, l2 with 
305

  
306
  (* Both lists are empty: return true *)
307
  | [], [] -> true
308

  
309
  (* First list is empty, but second list not: return true *)
310
  | [], _ -> true
311

  
312
  (* Second list is empty, but first list not: return false *)
313
  | _, [] -> false
314

  
315
  (* First and second head elements are physically equal: remove
316
     both head elements *)
317
  | h1 :: tl1, h2 :: tl2 when h1 == h2 -> list_subset_uniq cmp tl1 tl2
318

  
319
  (* First head element is smaller than second: return false *)
320
  | h1 :: tl, h2 :: _ when cmp h1 h2 < 0 -> false
321

  
322
  (* First head element is greater than the second or structurally
323
     but not physically equal: remove first head element *)
324
  | h1 :: _, h2 :: tl -> list_subset_uniq cmp l1 tl
325

  
326

  
327
(* Lexicographic comparison of pairs *)
328
let compare_pairs cmp_a cmp_b (a1, b1) (a2, b2) =
329
  let c_a = cmp_a a1 a2 in if c_a = 0 then cmp_b b1 b2 else c_a
330

  
331

  
332
(* Lexicographic comparison of lists *)
333
let rec compare_lists f l1 l2 = 
334

  
335
    match l1, l2 with 
336

  
337
      (* Two empty lists are equal *)
338
      | [], [] -> 0
339

  
340
      (* An empty list is smaller than a non-empty list *)
341
      | [], _ -> -1 
342

  
343
      (* An non-empty list is greater than an empty list *)
344
      | _, [] -> 1
345

  
346
      (* Compare two non-empty lists *)
347
      | h1 :: tl1, h2 :: tl2 -> 
348

  
349
        (* Compare head elements of lists *)
350
        let c = f h1 h2 in
351

  
352
        (* If head elements are equal, compare tails of lists,
353
           otherwise return comparison of head elements *)
354
        if c = 0 then compare_lists f tl1 tl2 else c
355

  
356

  
357
(* Given two ordered association lists with identical keys, push the
358
   values of each element of the first association list to the list of
359
   elements of the second association list. 
360

  
361
   The returned association list is in the order of the input lists,
362
   the function [equal] is used to compare keys. *)
363
let list_join equal l1 l2 = 
364

  
365
  let rec list_join' equal accum l1 l2 = match l1, l2 with
366
    
367
    (* Both lists consumed, return in original order *)
368
    | [], [] -> List.rev accum 
369
                  
370
    (* Keys of head elements in both lists equal *)
371
    | (((k1, v1) :: tl1), ((k2, v2) :: tl2)) when equal k1 k2 -> 
372
      
373
      (* Add to accumulator and continue *)
374
      list_join' equal ((k1, (v1 :: v2)) :: accum) tl1 tl2
375
        
376
    (* Keys of head elements different, or one of the lists is empty *)
377
    | _ -> failwith "list_join"
378
             
379
  in
380

  
381
  (* Second list is empty? *)
382
  match l2 with 
383

  
384
    (* Initialize with singleton elements from first list *)
385
    | [] -> List.map (fun (k, v) -> (k, [v])) l1
386

  
387
    (* Call recursive function with initial accumulator *)
388
    | _ -> list_join' equal [] l1 l2
389

  
390

  
391
(* ********************************************************************** *)
392
(* Array functions                                                        *)
393
(* ********************************************************************** *)
394

  
395
(* Returns the maximum element of a non-empty array *)
396
let array_max a =
397
  assert (Array.length a > 0);
398
  let max_val = ref a.(0) in
399
  Array.iter (fun x -> if x > !max_val then max_val := x else ()) a;
400
  !max_val
401

  
402
(* ********************************************************************** *)
403
(* Set functions                                                          *)
404
(* ********************************************************************** *)
405

  
406
(* Set of integers *)
407
module IntegerSet = 
408
  Set.Make
409
  (struct
410
    type t = int
411
    let compare = Pervasives.compare
412
    let equal = (=)
413
   end)
414
  
415
  
416
(* Hashtable of integers *)
417
module IntegerHashtbl =
418
  Hashtbl.Make
419
    (struct
420
      type t = int
421
      let hash i = i
422
      let equal = (=)
423
     end)
424

  
425
    
426
(* ********************************************************************** *)
427
(* Generic pretty-printing                                                 *)
428
(* ********************************************************************** *)
429

  
430
(* Pretty-print an array *)
431
let pp_print_arrayi pp sep ppf array  =
432
  let n = Array.length array in
433
  let print_element i =
434
    if i = n-1 then
435
      pp ppf i array.(i)
436
    else
437
      (pp ppf i array.(i);
438
       fprintf ppf sep)
439
  in
440
  let indices = list_init (fun i -> i) n in  
441
  List.iter print_element indices
442
  
443
(* Pretty-print a list *)
444
let rec pp_print_list pp sep ppf = function 
445

  
446
  (* Output nothing for the empty list *) 
447
  | [] -> ()
448

  
449
  (* Output a single element in the list  *) 
450
  | e :: [] -> 
451
    pp ppf e
452

  
453
  (* Output a single element and a space *) 
454
  | e :: tl -> 
455

  
456
    (* Output one element *)
457
    pp_print_list pp sep ppf [e]; 
458

  
459
    (* Output separator *)
460
    fprintf ppf sep; 
461

  
462
    (* Output the rest of the list *)
463
    pp_print_list pp sep ppf tl
464

  
465

  
466
  
467
(* Pretty-print a list with a counter of its elements *)
468
let rec pp_print_listi' pp sep ppf = function 
469

  
470
  (* Output nothing for the empty list *) 
471
  | (_, []) -> ()
472

  
473
  (* Output a single element in the list  *) 
474
  | (i, e :: []) -> pp ppf i e
475

  
476
  (* Output a single element and a space *) 
477
  | (i, e :: tl) -> 
478

  
479
    (* Output one element *)
480
    pp ppf i e;
481

  
482
    (* Output separator *)
483
    fprintf ppf sep; 
484

  
485
    (* Output the rest of the list *)
486
    pp_print_listi' pp sep ppf (succ i, tl)
487

  
488

  
489
(* Pretty-print a list with a counter of its elements *)
490
let pp_print_listi pp sep ppf l = pp_print_listi' pp sep ppf (0, l)
491

  
492

  
493

  
494
let rec pp_print_list2i' pp sep ppf = function 
495
  | _, [], [] -> ()
496
  | i, [e1], [e2] -> pp ppf i e1 e2
497
  | i, e1 :: tl1, e2 :: tl2 -> 
498
    pp ppf i e1 e2;
499
    (* Output separator *)
500
    fprintf ppf sep; 
501
    (* Output the rest of the two lists *)
502
    pp_print_list2i' pp sep ppf (succ i, tl1, tl2)
503
  | _ -> invalid_arg "pp_print_list2i"
504

  
505
(* Pretty-print two lists of the same length with a counter of their
506
   elements *)
507
let pp_print_list2i pp sep ppf l1 l2 = pp_print_list2i' pp sep ppf (0, l1, l2)
508

  
509

  
510
(* Pretty-print a list wrapped in parentheses *)
511
let pp_print_paren_list ppf list = 
512
      
513
  (* Begin expression with opening parenthesis *)
514
  pp_print_string ppf "(";
515
  
516
  (* Output elements of list *)
517
  pp_print_list pp_print_string "@ " ppf list;
518

  
519
  (* End expression with closing parenthesis *)
520
  pp_print_string ppf ")"
521

  
522

  
523
(* Pretty-print an option type *)
524
let pp_print_option pp ppf = function 
525
  | None -> fprintf ppf "None"
526
  | Some s -> fprintf ppf "@[<hv>Some@ %a@]" pp s
527

  
528

  
529
(* Print if list is not empty *)
530
let pp_print_if_not_empty s ppf = function 
531
  | [] -> ()
532
  | _ -> fprintf ppf s
533

  
534
(* Pretty-print into a string *)
535
let string_of_t pp t = 
536

  
537
  (* Create a buffer *)
538
  let buf = Buffer.create 80 in
539
  
540
  (* Create a formatter printing into the buffer *)
541
  let ppf = formatter_of_buffer buf in
542

  
543
  (* Output into buffer *)
544
  pp ppf t;
545
  
546
  (* Flush the formatter *)
547
  pp_print_flush ppf ();
548
  
549
  (* Return the buffer contents *)
550
  Buffer.contents buf
551

  
552

  
553
(* Return the strings as a parenthesized and space separated list *)
554
let paren_string_of_string_list list =
555
  string_of_t pp_print_paren_list list
556

  
557
(* Return the width of the string, meaning the wisth of it's longest line *)
558
let width_of_string s =
559
  let lines = Str.split (Str.regexp "\n") s in
560
  List.fold_left (fun max_width s ->
561
      max max_width (String.length s)
562
    ) 0 lines
563

  
564

  
565
(* ********************************************************************** *)
566
(* Option types                                                           *)
567
(* ********************************************************************** *)
568

  
569
(* Return the value of an option type, raise [Invalid_argument "get"]
570
   if the option value is [None] *)
571
let get = function None -> raise (Invalid_argument "get") | Some x -> x
572

  
573

  
574
(* ********************************************************************** *)
575
(* String                                                                 *)
576
(* ********************************************************************** *)
577

  
578

  
579

  
580
(* Return true if the first characters of [s1] up to the length of
581
   [s2] are ientical to [s2]. Return false if [s2] is longer than
582
   [s1]. *)
583
let string_starts_with s1 s2 = 
584
  (String.length s1 >= String.length s2) &&
585
  (String.sub s1 0 (String.length s2) = s2)
586

  
587

  
588

  
589
(* ********************************************************************** *)
590
(* Log levels                                                             *)
591
(* ********************************************************************** *)
592

  
593

  
594
(* Levels of log messages *)
595
type log_level =
596
  | L_off
597
  | L_fatal
598
  | L_error
599
  | L_warn
600
  | L_note
601
  | L_info
602
  | L_debug
603
  | L_trace
604

  
605
(* Default log level. *)
606
let default_log_level = L_note
607

  
608
(* Associate an integer with each level to induce a total ordering *)
609
let int_of_log_level = function 
610
  | L_off -> -1 
611
  | L_fatal -> 0
612
  | L_error -> 1
613
  | L_warn -> 2
614
  | L_note -> 3
615
  | L_info -> 4
616
  | L_debug -> 5
617
  | L_trace -> 6
618

  
619

  
620
let log_level_of_int = function 
621
  | -1 -> L_off 
622
  | 0 -> L_fatal
623
  | 1 -> L_error
624
  | 2 -> L_warn
625
  | 3 -> L_note
626
  | 4 -> L_info
627
  | 5 -> L_debug
628
  | 6 -> L_trace
629
  | _ -> raise (Invalid_argument "log_level_of_int")
630

  
631
let string_of_log_level = function
632
  | L_off -> "off"
633
  | L_fatal -> "fatal"
634
  | L_error -> "error"
635
  | L_warn -> "warn"
636
  | L_note -> "note"
637
  | L_info -> "info"
638
  | L_debug -> "debug"
639
  | L_trace -> "trace"
640

  
641

  
642

  
643
(* Compare two levels *)
644
let compare_levels l1 l2 = 
645
  Pervasives.compare (int_of_log_level l1) (int_of_log_level l2)
646

  
647

  
648
(* Current log level *)
649
let log_level = ref L_warn
650

  
651

  
652
(* Set log level *)
653
let set_log_level l = log_level := l
654
(* Log level *)
655
let get_log_level () = !log_level
656

  
657

  
658
(* Level is of higher or equal priority than current log level? *)
659
let output_on_level level = compare_levels level !log_level <= 0
660

  
661

  
662
(* Return fprintf if level is is of higher or equal priority
663
   than current log level, otherwise return ifprintf *)
664
let ignore_or_fprintf level = 
665
  if output_on_level level then fprintf else ifprintf
666

  
667

  
668
(* ********************************************************************** *)
669
(* Output target                                                          *)  
670
(* ********************************************************************** *)
671

  
672

  
673
(* Current formatter for output *)
674
let log_ppf = ref std_formatter
675

  
676

  
677
(* Set file to write log messages to *)
678
let log_to_file f = 
679

  
680
  (* Open channel to logfile *)
681
  let oc = 
682
    try open_out f with
683
      | Sys_error _ -> failwith "Could not open logfile"
684
  in 
685
  
686
  (* Create and store formatter for logfile *)
687
  log_ppf := formatter_of_out_channel oc
688

  
689

  
690
(* Write messages to standard output *)
691
let log_to_stdout () = log_ppf := std_formatter
692

  
693

  
694
(* ********************************************************************** *)
695
(* System functions                                                       *)
696
(* ********************************************************************** *)
697

  
698
(* let pp_print_banner ppf () = *)
699
(*     fprintf ppf "%s %s" Kind2Config.package_name Version.version *)
700

  
701
(* let pp_print_version ppf = pp_print_banner ppf () *)
702
  
703

  
704
(* Kind modules *)
705
type kind_module = 
706
  [ `IC3 
707
  | `BMC
708
  | `IND
709
  | `IND2
710
  | `INVGEN
711
  | `INVGENOS
712
  | `INVGENINT
713
  | `INVGENINTOS
714
  | `INVGENREAL
715
  | `INVGENREALOS
716
  | `C2I
717
  | `Interpreter
718
  | `Supervisor
719
  | `Parser
720
  | `Certif  ]
721

  
722

  
723
(* Pretty-print the type of the process *)
724
let pp_print_kind_module ppf = function
725
  | `IC3 -> fprintf ppf "property directed reachability"
726
  | `BMC -> fprintf ppf "bounded model checking"
727
  | `IND -> fprintf ppf "inductive step"
728
  | `IND2 -> fprintf ppf "2-induction"
729
  | `INVGEN -> fprintf ppf "two state invariant generator (bool)"
730
  | `INVGENOS -> fprintf ppf "one state invariant generator (bool)"
731
  | `INVGENINT -> fprintf ppf "two state invariant generator (int)"
732
  | `INVGENINTOS -> fprintf ppf "one state invariant generator (int)"
733
  | `INVGENREAL -> fprintf ppf "two state invariant generator (real)"
734
  | `INVGENREALOS -> fprintf ppf "one state invariant generator (real)"
735
  | `C2I -> fprintf ppf "c2i"
736
  | `Interpreter -> fprintf ppf "interpreter"
737
  | `Supervisor -> fprintf ppf "invariant manager"
738
  | `Parser -> fprintf ppf "parser"
739
  | `Certif -> Format.fprintf ppf "certificate"
740

  
741
(* String representation of a process type *)
742
let string_of_kind_module = string_of_t pp_print_kind_module
743

  
744

  
745
(* Return a short representation of kind module *)
746
let short_name_of_kind_module = function
747
 | `IC3 -> "ic3"
748
 | `BMC -> "bmc"
749
 | `IND -> "ind"
750
 | `IND2 -> "ind2"
751
 | `INVGEN -> "invgents"
752
 | `INVGENOS -> "invgenos"
753
 | `INVGENINT -> "invgenintts"
754
 | `INVGENINTOS -> "invgenintos"
755
 | `INVGENREAL -> "invgenintts"
756
 | `INVGENREALOS -> "invgenintos"
757
 | `C2I -> "c2i"
758
 | `Interpreter -> "interp"
759
 | `Supervisor -> "super"
760
 | `Parser -> "parse"
761
 | `Certif -> "certif"
762
                
763

  
764
(* Process type of a string *)
765
let kind_module_of_string = function 
766
  | "IC3" -> `IC3
767
  | "BMC" -> `BMC
768
  | "IND" -> `IND
769
  | "IND2" -> `IND2
770
  | "INVGEN" -> `INVGEN
771
  | "INVGENOS" -> `INVGENOS
772
  | "INVGENINT" -> `INVGENINT
773
  | "INVGENINTOS" -> `INVGENINTOS
774
  | "INVGENREAL" -> `INVGENREAL
775
  | "INVGENREALOS" -> `INVGENREALOS
776
  | "C2I" -> `C2I
777
  | _ -> raise (Invalid_argument "kind_module_of_string")
778

  
779

  
780
let int_of_kind_module = function
781
  | `Certif -> -4
782
  | `Parser -> -3
783
  | `Interpreter -> -2
784
  | `Supervisor -> -1
785
  | `BMC -> 1
786
  | `IND -> 2
787
  | `IND2 -> 3
788
  | `IC3 -> 4
789
  | `INVGEN -> 5
790
  | `INVGENOS -> 6
791
  | `INVGENINT -> 7
792
  | `INVGENINTOS -> 8
793
  | `INVGENREAL -> 9
794
  | `INVGENREALOS -> 10
795
  | `C2I -> 11
796

  
797

  
798
(* Timeouts *)
799
exception TimeoutWall
800
exception TimeoutVirtual
801

  
802
(* System signal caught *)
803
exception Signal of int
804

  
805
(* String representation of signal *)
806
let string_of_signal = function 
807
  | s when s = Sys.sigabrt -> "SIGABRT"
808
  | s when s = Sys.sigalrm -> "SIGALRM"
809
  | s when s = Sys.sigfpe -> "SIGFPE"
810
  | s when s = Sys.sighup -> "SIGHUP"
811
  | s when s = Sys.sigill -> "SIGILL"
812
  | s when s = Sys.sigint -> "SIGINT"
813
  | s when s = Sys.sigkill -> "SIGKILL"
814
  | s when s = Sys.sigpipe -> "SIGPIPE"
815
  | s when s = Sys.sigquit -> "SIGQUIT"
816
  | s when s = Sys.sigsegv -> "SIGSEGV"
817
  | s when s = Sys.sigterm -> "SIGTERM"
818
  | s when s = Sys.sigusr1 -> "SIGUSR1"
819
  | s when s = Sys.sigusr2 -> "SIGUSR2"
820
  | s when s = Sys.sigchld -> "SIGCHLD"
821
  | s when s = Sys.sigcont -> "SIGCONT"
822
  | s when s = Sys.sigstop -> "SIGSTOP"
823
  | s when s = Sys.sigtstp -> "SIGTSTP"
824
  | s when s = Sys.sigttin -> "SIGTTIN"
825
  | s when s = Sys.sigttou -> "SIGTTOU"
826
  | s when s = Sys.sigvtalrm -> "SIGVTALRM"
827
  | s when s = Sys.sigprof -> "SIGPROF"
828
  | s -> string_of_int s
829

  
830
let pp_print_signal ppf s = fprintf ppf "%s" (string_of_signal s)
831

  
832
(* Pretty-print the termination status of a process *)
833
let pp_print_process_status ppf = function 
834
  | Unix.WEXITED s -> fprintf ppf "exited with return code %d" s
835

  
836
  | Unix.WSIGNALED s -> 
837
    fprintf ppf "killed by signal %a" pp_print_signal s
838

  
839
  | Unix.WSTOPPED s -> 
840
    fprintf ppf "stopped by signal %a" pp_print_signal s
841

  
842

  
843
(* Raise exception on signal *)
844
let exception_on_signal signal = 
845
  (* printf "Signal %a caught" pp_print_signal signal; *)
846
  raise (Signal signal)
847

  
848

  
849
(* (\* Sleep for seconds, resolution is in ms *\) *)
850
(* let minisleep sec = *)
851

  
852
(*   try  *)
853

  
854
(*     (\* Sleep for the given seconds, yield to other threads *\) *)
855
(*     Thread.delay sec  *)
856

  
857
(*   with  *)
858

  
859
(*     (\* Signal caught while in kernel *\) *)
860
(*     | Unix.Unix_error(Unix.EINTR, _, _) ->  *)
861

  
862
(*       (\* Cannot find out signal number *\) *)
863
(*       raise (Signal 0) *)
864

  
865

  
866
(* Return full path to executable, search PATH environment variable
867
   and current working directory *)
868
let find_on_path exec = 
869

  
870
  let rec find_on_path' exec path = 
871

  
872
    (* Terminate on empty path *)
873
    if path = "" then raise Not_found;
874

  
875
    (* Split path at first colon *)
876
    let path_hd, path_tl = 
877

  
878
      try 
879

  
880
        (* Position of colon in string *)
881
        let colon_index = String.index path ':' in
882

  
883
        (* Length of string *)
884
        let path_len = String.length path in
885

  
886
        (* Return string up to colon *)
887
        (String.sub path 0 colon_index, 
888
         
889
         (* Return string after colon *)
890
         String.sub path (colon_index + 1) (path_len - colon_index - 1))
891

  
892
      (* Colon not found, return whole string and empty string *)
893
      with Not_found -> path, ""
894

  
895
    in
896
    
897
    (* Combine path and filename *)
898
    let exec_path = Filename.concat path_hd exec in
899
    
900
    if 
901

  
902
      (* Check if file exists on path *)
903
      Sys.file_exists exec_path 
904

  
905
    then 
906

  
907
      (* Return full path to file 
908

  
909
         TODO: Check if file is executable here? *)
910
      exec_path 
911

  
912
    else 
913

  
914
      (* Continue on remaining path entries *)
915
      find_on_path' exec path_tl
916

  
917
  in
918

  
919
  try 
920

  
921
    if Filename.is_relative exec then 
922

  
923
      (* Return filename on path, fail with Not_found if path is empty
924
         or [exec] not found on path *)
925
      find_on_path' exec (Unix.getenv "PATH")
926
        
927
    else if 
928
      
929
      (* Check if file exists on path *)
930
      Sys.file_exists exec
931
        
932
    then 
933
      
934
      (* Return full path to file 
935
         
936
         TODO: Check if file is executable here? *)
937
      exec
938

  
939
    else 
940

  
941
      raise Not_found
942

  
943
  with Not_found -> 
944

  
945
    (* Check current directory as last resort *)
946
    let exec_path = Filename.concat (Sys.getcwd ()) exec in 
947

  
948
    (* Return full path if file exists, fail otherwise *)
949
    if Sys.file_exists exec_path then exec_path else raise Not_found
950

  
951
(* ********************************************************************** *)
952
(* Parser and lexer functions                                             *)
953
(* ********************************************************************** *)
954

  
955

  
956
(* A position in a file
957

  
958
   The column is the actual colum number, not an offset from the
959
   beginning of the file as in Lexing.position *)
960
type position =
961
  { pos_fname : string; pos_lnum: int; pos_cnum: int }
962

  
963

  
964
(* Comparision on positions *)
965
let compare_pos 
966
    { pos_fname = p1; pos_lnum = l1; pos_cnum = c1 }  
967
    { pos_fname = p2; pos_lnum = l2; pos_cnum = c2 } =
968

  
969
  compare_pairs 
970
    String.compare
971
    (compare_pairs Pervasives.compare Pervasives.compare)
972
    (p1, (l1, c1)) 
973
    (p2, (l2, c2)) 
974

  
975

  
976
(* A dummy position, different from any valid position *)
977
let dummy_pos = { pos_fname = ""; pos_lnum = 0; pos_cnum = -1 }
978

  
979

  
980
(* A dummy position in the specified file *)
981
let dummy_pos_in_file fname = 
982
  { pos_fname = fname; pos_lnum = 0; pos_cnum = -1 }
983

  
984

  
985
(* Pretty-print a position *)
986
let pp_print_position ppf (
987
  { pos_fname; pos_lnum; pos_cnum } as pos
988
) =
989

  
990
  if pos = dummy_pos then 
991

  
992
    fprintf ppf "(unknown)"
993

  
994
  else if pos_lnum = 0 && pos_cnum = -1 then
995

  
996
    fprintf ppf "%s" pos_fname
997

  
998
  else if pos_fname <> "" then
999

  
1000
    fprintf ppf "%s:%d:%d" pos_fname pos_lnum pos_cnum
1001

  
1002
  else
1003

  
1004
    fprintf 
1005
      ppf
1006
      "@[<hv>line %d@ col. %d@]"
1007
      pos_lnum
1008
      pos_cnum
1009

  
1010

  
1011
(* Pretty-print a position *)
1012
let pp_print_pos ppf (
1013
  { pos_fname; pos_lnum; pos_cnum } as pos
1014
) =
1015

  
1016
  if pos = dummy_pos then 
1017

  
1018
    fprintf ppf "[unknown]"
1019

  
1020
  else if pos_lnum = 0 && pos_cnum = -1 then
1021

  
1022
    fprintf ppf "%s" pos_fname
1023

  
1024
  else
1025

  
1026
    fprintf 
1027
      ppf
1028
      "[%tl%dc%d]"
1029
      (function ppf -> 
1030
        if pos_fname = "" then () else fprintf ppf "%s|" pos_fname)
1031
      pos_lnum
1032
      pos_cnum
1033

  
1034

  
1035
(* Convert a position from Lexing to a position *)
1036
let position_of_lexing 
1037
    { Lexing.pos_fname;
1038
      Lexing.pos_lnum;
1039
      Lexing.pos_bol;
1040
      Lexing.pos_cnum } = 
1041

  
1042
  (* Colum number is relative to the beginning of the file *)
1043
  { pos_fname = pos_fname; 
1044
    pos_lnum = pos_lnum; 
1045
    pos_cnum = pos_cnum - pos_bol } 
1046

  
1047

  
1048
(* Return true if position is a dummy position *)
1049
let is_dummy_pos = function 
1050
  | { pos_cnum = -1 } -> true 
1051
  | _ -> false
1052

  
1053

  
1054
(* Return the file, line and column of a position; fail if the
1055
   position is a dummy position *)
1056
let file_row_col_of_pos = function 
1057

  
1058
  (* Fail if position is a dummy position *)
1059
  | p when is_dummy_pos p -> raise (Invalid_argument "file_row_col_of_pos")
1060

  
1061
  (* Return tuple of filename, line and column *)
1062
  | { pos_fname; pos_lnum; pos_cnum } -> (pos_fname, pos_lnum, pos_cnum)
1063

  
1064

  
1065
let print_backtrace fmt bt =
1066
  match Printexc.backtrace_slots bt with
1067
  | None -> ()
1068
  | Some slots ->
1069
    let n = Array.length slots in
1070
    Array.iteri (fun i s ->
1071
        match Printexc.Slot.format i s with
1072
        | None -> ()
1073
        | Some s ->
1074
          pp_print_string fmt s;
1075
          if i < n - 1 then pp_force_newline fmt ()
1076
      ) slots
1077

  
1078

  
1079
let pos_of_file_row_col (pos_fname, pos_lnum, pos_cnum) =
1080
  { pos_fname; pos_lnum; pos_cnum }
1081

  
1082

  
1083
(* Split a string at its first dot. Raises {Not_found} if there are not dots *)
1084
let split_dot s =
1085
  let open String in
1086
  let n = (index s '.') in
1087
  sub s 0 n, sub s (n+1) (length s - n - 1)
1088

  
1089

  
1090
(* Extract scope from a concatenated name *)
1091
let extract_scope_name name =
1092

  
1093
  let rec loop s scope =
1094
    try
1095
      let next_scope, s' = split_dot s in
1096
      loop s' (next_scope :: scope)
1097
    with Not_found -> s, List.rev scope
1098
  in
1099
  loop name []
1100

  
1101

  
1102

  
1103
(* Create a directory if it does not already exists. *)
1104
let create_dir dir =
1105
  try if not (Sys.is_directory dir) then failwith (dir^" is not a directory")
1106
  with Sys_error _ -> Unix.mkdir dir 0o755
1107

  
1108

  
1109
(* Copy file.
1110

  
1111
   Implementation adapted from "Unix system programming in OCaml" by Xavier
1112
   Leroy and Didier Remy*)
1113

  
1114

  
1115

  
1116
let copy_fds fd_in fd_out =
1117
  let open Unix in
1118
  let buffer_size = 8192 in
1119
  let buffer = Bytes.create buffer_size in
1120
  let rec copy_loop () = match read fd_in buffer 0 buffer_size with
1121
    | 0 -> ()
1122
    | r -> ignore (write fd_out buffer 0 r); copy_loop ()
1123
  in
1124
  copy_loop ()
1125
  
1126

  
1127
let file_copy input_name output_name =
1128
  let open Unix in
1129
  let fd_in = openfile input_name [O_RDONLY] 0 in
1130
  let fd_out = openfile output_name [O_WRONLY; O_CREAT; O_TRUNC] 0o666 in
1131
  copy_fds fd_in fd_out;
1132
  close fd_in;
1133
  close fd_out
1134

  
1135

  
1136
let files_cat_open ?(add_prefix=fun _ -> ()) files output_name =
1137
  let open Unix in
1138
  let fd_out = openfile output_name [O_WRONLY; O_CREAT; O_TRUNC] 0o666 in
1139
  add_prefix (out_channel_of_descr fd_out |> Format.formatter_of_out_channel);
1140
  let _, fd_out =
1141
    List.fold_left (fun (first, fd_out) input_name ->
1142
        let fd_in = openfile input_name [O_RDONLY] 0 in
1143
        copy_fds fd_in fd_out;
1144
        let fd_out =
1145
          if first then begin
1146
            close fd_out;
1147
            openfile output_name [O_WRONLY; O_CREAT; O_APPEND] 0o666
1148
          end
1149
          else fd_out in
1150
        false, fd_out
1151
      )
1152
      (true, fd_out)
1153
      files
1154
  in
1155
  fd_out
1156

  
1157

  
1158
(* Captures the output and exit status of a unix command : aux func *)
1159
let syscall cmd =
1160
  let ic, oc = Unix.open_process cmd in
1161
  let buf = Buffer.create 16 in
1162
  (try
1163
     while true do
1164
       Buffer.add_channel buf ic 1
1165
     done
1166
   with End_of_file -> ());
1167
  ignore(Unix.close_process (ic, oc));
1168
  Buffer.contents buf
1169

  
1170

  
1171

  
1172
let reset_gc_params =
1173
  let gc_c = Gc.get() in
1174
  fun () -> Gc.set gc_c
1175
  
1176

  
1177
let set_liberal_gc () =
1178
  Gc.full_major ();
1179
  let gc_c =
1180
    { (Gc.get ()) with
1181
      (* Gc.verbose = 0x3FF; *)
1182
      Gc.minor_heap_size = 64000000; (* default 32000*)
1183
      major_heap_increment = 3200000;    (* default 124000*)
1184
      space_overhead = 100; (* default 80% des donnes vivantes *)
1185
    }
1186
  in
1187
  Gc.set gc_c
1188

  
1189

  
1190
(* ********************************************************************** *)
1191
(* Paths techniques write to                                              *)
1192
(* ********************************************************************** *)
1193

  
1194
module Paths = struct
1195
  let testgen = "tests"
1196
  let oracle = "oracle"
1197
  let implem = "implem"
1198
end
1199

  
1200
(* ********************************************************************** *)
1201
(* Reserved identifiers                                                   *)
1202
(* ********************************************************************** *)
1203

  
1204
module ReservedIds = struct
1205

  
1206
  let abs_ident_string = "abs"
1207
  let oracle_ident_string = "nondet"
1208
  let instance_ident_string = "instance"
1209
  let init_flag_ident_string = "init_flag"
1210
  let all_req_ident_string = "all_req"
1211
  let all_ens_ident_string = "all_ens"
1212
  let inst_ident_string = "inst"
1213
  let init_uf_string = "__node_init"
1214
  let trans_uf_string = "__node_trans"
1215
  let index_ident_string = "__index"
1216
  let function_of_inputs = "__function_of_inputs"
1217

  
1218
  let state_string = "state"
1219
  let restart_string = "restart"
1220
  let state_selected_string = "state.selected"
1221
  let restart_selected_string = "restart.selected"
1222
  let state_selected_next_string = "state.selected.next"
1223
  let restart_selected_next_string = "restart.selected.next"
1224
  let handler_string = "handler"
1225
  let unless_string = "unless"
1226
  
1227
  (* Init flag string. *)
1228
  let init_flag_string = "__init_flag"
1229
  (* Abstraction depth input string. *)
1230
  let depth_input_string = "__depth_input"
1231
  (* Abstraction depth input string. *)
1232
  let max_depth_input_string = "__max_depth_input"
1233

  
1234
  let reserved_strings = [
1235
    init_flag_string ;
1236
    depth_input_string ;
1237
    max_depth_input_string ;
1238
    function_of_inputs ;
1239

  
1240
    abs_ident_string ;
1241
    oracle_ident_string ;
1242
    instance_ident_string ;
1243
    init_flag_ident_string ;
1244
    all_req_ident_string ;
1245
    all_ens_ident_string ;
1246
    inst_ident_string ;
1247
    init_uf_string ;
1248
    trans_uf_string ;
1249
    index_ident_string ;
1250
  ]
1251

  
1252
end
1253

  
1254

  
1255
(* |===| Exit codes. *)
1256

  
1257
(** Exit codes. *)
1258
module ExitCodes = struct
1259
  let unknown = 0
1260
  let unsafe = 10
1261
  let safe = 20
1262
  let error = 2
1263
  let kid_status = 128
1264
end
1265

  
1266

  
1267
(* |===| File names. *)
1268

  
1269
(** File names. *)
1270
module Names = struct
1271
  (** Contract generation file. *)
1272
  let contract_gen_file = "kind2_contract.lus"
1273
  (** Contract name for contract generation. *)
1274
  let contract_name =
1275
    Format.asprintf "%a_spec" (pp_print_list Format.pp_print_string "_")
1276
  (** Invariant logging file. *)
1277
  let inv_log_file = "kind2_strengthening.lus"
1278
  (** Contract name for invariant logging. *)
1279
  let inv_log_contract_name =
1280
    Format.asprintf "%a_str_spec" (pp_print_list Format.pp_print_string "_")
1281
end
1282

  
1283

  
1284
(* 
1285
   Local Variables:
1286
   compile-command: "make -C .. -k"
1287
   tuareg-interactive-program: "./kind2.top -I ./_build -I ./_build/SExpr"
1288
   indent-tabs-mode: nil
1289
   End: 
1290
*)
src/cocospec/kindLib.mli
1
(* This file is part of the Kind 2 model checker.
2

  
3
   Copyright (c) 2015 by the Board of Trustees of the University of Iowa
4

  
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff