src/HOL/SMT_Examples/VCC_Max.b2i
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 52722 2c81f7baf8c4
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
boehmes@52722
     1
type-decl $ctype 0 0
boehmes@52722
     2
type-decl $ptr 0 0
boehmes@52722
     3
type-decl $field 0 0
boehmes@52722
     4
type-decl $kind 0 0
boehmes@52722
     5
type-decl $type_state 0 0
boehmes@52722
     6
type-decl $status 0 0
boehmes@52722
     7
type-decl $primitive 0 0
boehmes@52722
     8
type-decl $struct 0 0
boehmes@52722
     9
type-decl $token 0 0
boehmes@52722
    10
type-decl $state 0 0
boehmes@52722
    11
type-decl $pure_function 0 0
boehmes@52722
    12
type-decl $label 0 0
boehmes@52722
    13
type-decl $memory_t 0 0
boehmes@52722
    14
type-decl $typemap_t 0 0
boehmes@52722
    15
type-decl $statusmap_t 0 0
boehmes@52722
    16
type-decl $record 0 0
boehmes@52722
    17
type-decl $version 0 0
boehmes@52722
    18
type-decl $vol_version 0 0
boehmes@52722
    19
type-decl $ptrset 0 0
boehmes@52722
    20
fun-decl $kind_of 2 0
boehmes@52722
    21
    type-con $ctype 0
boehmes@52722
    22
    type-con $kind 0
boehmes@52722
    23
fun-decl $kind_composite 1 1
boehmes@52722
    24
    type-con $kind 0
boehmes@52722
    25
  attribute unique 0
boehmes@52722
    26
fun-decl $kind_primitive 1 1
boehmes@52722
    27
    type-con $kind 0
boehmes@52722
    28
  attribute unique 0
boehmes@52722
    29
fun-decl $kind_array 1 1
boehmes@52722
    30
    type-con $kind 0
boehmes@52722
    31
  attribute unique 0
boehmes@52722
    32
fun-decl $kind_thread 1 1
boehmes@52722
    33
    type-con $kind 0
boehmes@52722
    34
  attribute unique 0
boehmes@52722
    35
fun-decl $sizeof 2 0
boehmes@52722
    36
    type-con $ctype 0
boehmes@52722
    37
    int
boehmes@52722
    38
fun-decl ^^i1 1 1
boehmes@52722
    39
    type-con $ctype 0
boehmes@52722
    40
  attribute unique 0
boehmes@52722
    41
fun-decl ^^i2 1 1
boehmes@52722
    42
    type-con $ctype 0
boehmes@52722
    43
  attribute unique 0
boehmes@52722
    44
fun-decl ^^i4 1 1
boehmes@52722
    45
    type-con $ctype 0
boehmes@52722
    46
  attribute unique 0
boehmes@52722
    47
fun-decl ^^i8 1 1
boehmes@52722
    48
    type-con $ctype 0
boehmes@52722
    49
  attribute unique 0
boehmes@52722
    50
fun-decl ^^u1 1 1
boehmes@52722
    51
    type-con $ctype 0
boehmes@52722
    52
  attribute unique 0
boehmes@52722
    53
fun-decl ^^u2 1 1
boehmes@52722
    54
    type-con $ctype 0
boehmes@52722
    55
  attribute unique 0
boehmes@52722
    56
fun-decl ^^u4 1 1
boehmes@52722
    57
    type-con $ctype 0
boehmes@52722
    58
  attribute unique 0
boehmes@52722
    59
fun-decl ^^u8 1 1
boehmes@52722
    60
    type-con $ctype 0
boehmes@52722
    61
  attribute unique 0
boehmes@52722
    62
fun-decl ^^void 1 1
boehmes@52722
    63
    type-con $ctype 0
boehmes@52722
    64
  attribute unique 0
boehmes@52722
    65
fun-decl ^^bool 1 1
boehmes@52722
    66
    type-con $ctype 0
boehmes@52722
    67
  attribute unique 0
boehmes@52722
    68
fun-decl ^^f4 1 1
boehmes@52722
    69
    type-con $ctype 0
boehmes@52722
    70
  attribute unique 0
boehmes@52722
    71
fun-decl ^^f8 1 1
boehmes@52722
    72
    type-con $ctype 0
boehmes@52722
    73
  attribute unique 0
boehmes@52722
    74
fun-decl ^^claim 1 1
boehmes@52722
    75
    type-con $ctype 0
boehmes@52722
    76
  attribute unique 0
boehmes@52722
    77
fun-decl ^^root_emb 1 1
boehmes@52722
    78
    type-con $ctype 0
boehmes@52722
    79
  attribute unique 0
boehmes@52722
    80
fun-decl ^^mathint 1 1
boehmes@52722
    81
    type-con $ctype 0
boehmes@52722
    82
  attribute unique 0
boehmes@52722
    83
fun-decl ^$#thread_id_t 1 1
boehmes@52722
    84
    type-con $ctype 0
boehmes@52722
    85
  attribute unique 0
boehmes@52722
    86
fun-decl ^$#ptrset 1 1
boehmes@52722
    87
    type-con $ctype 0
boehmes@52722
    88
  attribute unique 0
boehmes@52722
    89
fun-decl ^$#state_t 1 1
boehmes@52722
    90
    type-con $ctype 0
boehmes@52722
    91
  attribute unique 0
boehmes@52722
    92
fun-decl ^$#struct 1 1
boehmes@52722
    93
    type-con $ctype 0
boehmes@52722
    94
  attribute unique 0
boehmes@52722
    95
fun-decl $ptr_to 2 0
boehmes@52722
    96
    type-con $ctype 0
boehmes@52722
    97
    type-con $ctype 0
boehmes@52722
    98
fun-decl $unptr_to 2 0
boehmes@52722
    99
    type-con $ctype 0
boehmes@52722
   100
    type-con $ctype 0
boehmes@52722
   101
fun-decl $ptr_level 2 0
boehmes@52722
   102
    type-con $ctype 0
boehmes@52722
   103
    int
boehmes@52722
   104
fun-decl $map_t 3 0
boehmes@52722
   105
    type-con $ctype 0
boehmes@52722
   106
    type-con $ctype 0
boehmes@52722
   107
    type-con $ctype 0
boehmes@52722
   108
fun-decl $map_domain 2 0
boehmes@52722
   109
    type-con $ctype 0
boehmes@52722
   110
    type-con $ctype 0
boehmes@52722
   111
fun-decl $map_range 2 0
boehmes@52722
   112
    type-con $ctype 0
boehmes@52722
   113
    type-con $ctype 0
boehmes@52722
   114
fun-decl $is_primitive 2 1
boehmes@52722
   115
    type-con $ctype 0
boehmes@52722
   116
    bool
boehmes@52722
   117
  attribute weight 1
boehmes@52722
   118
    expr-attr
boehmes@52722
   119
      int-num 0
boehmes@52722
   120
fun-decl $is_primitive_ch 2 1
boehmes@52722
   121
    type-con $ctype 0
boehmes@52722
   122
    bool
boehmes@52722
   123
  attribute inline 1
boehmes@52722
   124
    expr-attr
boehmes@52722
   125
      true
boehmes@52722
   126
fun-decl $is_composite 2 1
boehmes@52722
   127
    type-con $ctype 0
boehmes@52722
   128
    bool
boehmes@52722
   129
  attribute weight 1
boehmes@52722
   130
    expr-attr
boehmes@52722
   131
      int-num 0
boehmes@52722
   132
fun-decl $is_composite_ch 2 1
boehmes@52722
   133
    type-con $ctype 0
boehmes@52722
   134
    bool
boehmes@52722
   135
  attribute inline 1
boehmes@52722
   136
    expr-attr
boehmes@52722
   137
      true
boehmes@52722
   138
fun-decl $is_arraytype 2 1
boehmes@52722
   139
    type-con $ctype 0
boehmes@52722
   140
    bool
boehmes@52722
   141
  attribute weight 1
boehmes@52722
   142
    expr-attr
boehmes@52722
   143
      int-num 0
boehmes@52722
   144
fun-decl $is_arraytype_ch 2 1
boehmes@52722
   145
    type-con $ctype 0
boehmes@52722
   146
    bool
boehmes@52722
   147
  attribute inline 1
boehmes@52722
   148
    expr-attr
boehmes@52722
   149
      true
boehmes@52722
   150
fun-decl $is_threadtype 2 1
boehmes@52722
   151
    type-con $ctype 0
boehmes@52722
   152
    bool
boehmes@52722
   153
  attribute weight 1
boehmes@52722
   154
    expr-attr
boehmes@52722
   155
      int-num 0
boehmes@52722
   156
fun-decl $is_thread 2 1
boehmes@52722
   157
    type-con $ptr 0
boehmes@52722
   158
    bool
boehmes@52722
   159
  attribute inline 1
boehmes@52722
   160
    expr-attr
boehmes@52722
   161
      true
boehmes@52722
   162
fun-decl $is_ptr_to_composite 2 1
boehmes@52722
   163
    type-con $ptr 0
boehmes@52722
   164
    bool
boehmes@52722
   165
  attribute inline 1
boehmes@52722
   166
    expr-attr
boehmes@52722
   167
      true
boehmes@52722
   168
fun-decl $field_offset 2 0
boehmes@52722
   169
    type-con $field 0
boehmes@52722
   170
    int
boehmes@52722
   171
fun-decl $field_parent_type 2 0
boehmes@52722
   172
    type-con $field 0
boehmes@52722
   173
    type-con $ctype 0
boehmes@52722
   174
fun-decl $is_non_primitive 2 0
boehmes@52722
   175
    type-con $ctype 0
boehmes@52722
   176
    bool
boehmes@52722
   177
fun-decl $is_non_primitive_ch 2 1
boehmes@52722
   178
    type-con $ctype 0
boehmes@52722
   179
    bool
boehmes@52722
   180
  attribute inline 1
boehmes@52722
   181
    expr-attr
boehmes@52722
   182
      true
boehmes@52722
   183
fun-decl $is_non_primitive_ptr 2 1
boehmes@52722
   184
    type-con $ptr 0
boehmes@52722
   185
    bool
boehmes@52722
   186
  attribute inline 1
boehmes@52722
   187
    expr-attr
boehmes@52722
   188
      true
boehmes@52722
   189
fun-decl $me_ref 1 0
boehmes@52722
   190
    int
boehmes@52722
   191
fun-decl $me 1 0
boehmes@52722
   192
    type-con $ptr 0
boehmes@52722
   193
fun-decl $current_state 2 1
boehmes@52722
   194
    type-con $state 0
boehmes@52722
   195
    type-con $state 0
boehmes@52722
   196
  attribute inline 1
boehmes@52722
   197
    expr-attr
boehmes@52722
   198
      true
boehmes@52722
   199
fun-decl $select.mem 3 0
boehmes@52722
   200
    type-con $memory_t 0
boehmes@52722
   201
    type-con $ptr 0
boehmes@52722
   202
    int
boehmes@52722
   203
fun-decl $store.mem 4 0
boehmes@52722
   204
    type-con $memory_t 0
boehmes@52722
   205
    type-con $ptr 0
boehmes@52722
   206
    int
boehmes@52722
   207
    type-con $memory_t 0
boehmes@52722
   208
fun-decl $select.tm 3 0
boehmes@52722
   209
    type-con $typemap_t 0
boehmes@52722
   210
    type-con $ptr 0
boehmes@52722
   211
    type-con $type_state 0
boehmes@52722
   212
fun-decl $store.tm 4 0
boehmes@52722
   213
    type-con $typemap_t 0
boehmes@52722
   214
    type-con $ptr 0
boehmes@52722
   215
    type-con $type_state 0
boehmes@52722
   216
    type-con $typemap_t 0
boehmes@52722
   217
fun-decl $select.sm 3 0
boehmes@52722
   218
    type-con $statusmap_t 0
boehmes@52722
   219
    type-con $ptr 0
boehmes@52722
   220
    type-con $status 0
boehmes@52722
   221
fun-decl $store.sm 4 0
boehmes@52722
   222
    type-con $statusmap_t 0
boehmes@52722
   223
    type-con $ptr 0
boehmes@52722
   224
    type-con $status 0
boehmes@52722
   225
    type-con $statusmap_t 0
boehmes@52722
   226
fun-decl $memory 2 0
boehmes@52722
   227
    type-con $state 0
boehmes@52722
   228
    type-con $memory_t 0
boehmes@52722
   229
fun-decl $typemap 2 0
boehmes@52722
   230
    type-con $state 0
boehmes@52722
   231
    type-con $typemap_t 0
boehmes@52722
   232
fun-decl $statusmap 2 0
boehmes@52722
   233
    type-con $state 0
boehmes@52722
   234
    type-con $statusmap_t 0
boehmes@52722
   235
fun-decl $mem 3 1
boehmes@52722
   236
    type-con $state 0
boehmes@52722
   237
    type-con $ptr 0
boehmes@52722
   238
    int
boehmes@52722
   239
  attribute inline 1
boehmes@52722
   240
    expr-attr
boehmes@52722
   241
      true
boehmes@52722
   242
fun-decl $read_any 3 1
boehmes@52722
   243
    type-con $state 0
boehmes@52722
   244
    type-con $ptr 0
boehmes@52722
   245
    int
boehmes@52722
   246
  attribute inline 1
boehmes@52722
   247
    expr-attr
boehmes@52722
   248
      true
boehmes@52722
   249
fun-decl $mem_eq 4 1
boehmes@52722
   250
    type-con $state 0
boehmes@52722
   251
    type-con $state 0
boehmes@52722
   252
    type-con $ptr 0
boehmes@52722
   253
    bool
boehmes@52722
   254
  attribute inline 1
boehmes@52722
   255
    expr-attr
boehmes@52722
   256
      true
boehmes@52722
   257
fun-decl $st_eq 4 1
boehmes@52722
   258
    type-con $state 0
boehmes@52722
   259
    type-con $state 0
boehmes@52722
   260
    type-con $ptr 0
boehmes@52722
   261
    bool
boehmes@52722
   262
  attribute inline 1
boehmes@52722
   263
    expr-attr
boehmes@52722
   264
      true
boehmes@52722
   265
fun-decl $ts_eq 4 1
boehmes@52722
   266
    type-con $state 0
boehmes@52722
   267
    type-con $state 0
boehmes@52722
   268
    type-con $ptr 0
boehmes@52722
   269
    bool
boehmes@52722
   270
  attribute inline 1
boehmes@52722
   271
    expr-attr
boehmes@52722
   272
      true
boehmes@52722
   273
fun-decl $extent_hint 3 0
boehmes@52722
   274
    type-con $ptr 0
boehmes@52722
   275
    type-con $ptr 0
boehmes@52722
   276
    bool
boehmes@52722
   277
fun-decl $nesting_level 2 0
boehmes@52722
   278
    type-con $ctype 0
boehmes@52722
   279
    int
boehmes@52722
   280
fun-decl $is_nested 3 0
boehmes@52722
   281
    type-con $ctype 0
boehmes@52722
   282
    type-con $ctype 0
boehmes@52722
   283
    bool
boehmes@52722
   284
fun-decl $nesting_min 3 0
boehmes@52722
   285
    type-con $ctype 0
boehmes@52722
   286
    type-con $ctype 0
boehmes@52722
   287
    int
boehmes@52722
   288
fun-decl $nesting_max 3 0
boehmes@52722
   289
    type-con $ctype 0
boehmes@52722
   290
    type-con $ctype 0
boehmes@52722
   291
    int
boehmes@52722
   292
fun-decl $is_nested_range 5 0
boehmes@52722
   293
    type-con $ctype 0
boehmes@52722
   294
    type-con $ctype 0
boehmes@52722
   295
    int
boehmes@52722
   296
    int
boehmes@52722
   297
    bool
boehmes@52722
   298
fun-decl $typ 2 0
boehmes@52722
   299
    type-con $ptr 0
boehmes@52722
   300
    type-con $ctype 0
boehmes@52722
   301
fun-decl $ref 2 0
boehmes@52722
   302
    type-con $ptr 0
boehmes@52722
   303
    int
boehmes@52722
   304
fun-decl $ptr 3 0
boehmes@52722
   305
    type-con $ctype 0
boehmes@52722
   306
    int
boehmes@52722
   307
    type-con $ptr 0
boehmes@52722
   308
fun-decl $ghost_ref 3 0
boehmes@52722
   309
    type-con $ptr 0
boehmes@52722
   310
    type-con $field 0
boehmes@52722
   311
    int
boehmes@52722
   312
fun-decl $ghost_emb 2 0
boehmes@52722
   313
    int
boehmes@52722
   314
    type-con $ptr 0
boehmes@52722
   315
fun-decl $ghost_path 2 0
boehmes@52722
   316
    int
boehmes@52722
   317
    type-con $field 0
boehmes@52722
   318
fun-decl $physical_ref 3 0
boehmes@52722
   319
    type-con $ptr 0
boehmes@52722
   320
    type-con $field 0
boehmes@52722
   321
    int
boehmes@52722
   322
fun-decl $array_path 3 0
boehmes@52722
   323
    type-con $field 0
boehmes@52722
   324
    int
boehmes@52722
   325
    type-con $field 0
boehmes@52722
   326
fun-decl $is_base_field 2 0
boehmes@52722
   327
    type-con $field 0
boehmes@52722
   328
    bool
boehmes@52722
   329
fun-decl $array_path_1 2 0
boehmes@52722
   330
    type-con $field 0
boehmes@52722
   331
    type-con $field 0
boehmes@52722
   332
fun-decl $array_path_2 2 0
boehmes@52722
   333
    type-con $field 0
boehmes@52722
   334
    int
boehmes@52722
   335
fun-decl $null 1 0
boehmes@52722
   336
    type-con $ptr 0
boehmes@52722
   337
fun-decl $is 3 0
boehmes@52722
   338
    type-con $ptr 0
boehmes@52722
   339
    type-con $ctype 0
boehmes@52722
   340
    bool
boehmes@52722
   341
fun-decl $ptr_cast 3 1
boehmes@52722
   342
    type-con $ptr 0
boehmes@52722
   343
    type-con $ctype 0
boehmes@52722
   344
    type-con $ptr 0
boehmes@52722
   345
  attribute inline 1
boehmes@52722
   346
    expr-attr
boehmes@52722
   347
      true
boehmes@52722
   348
fun-decl $read_ptr 4 1
boehmes@52722
   349
    type-con $state 0
boehmes@52722
   350
    type-con $ptr 0
boehmes@52722
   351
    type-con $ctype 0
boehmes@52722
   352
    type-con $ptr 0
boehmes@52722
   353
  attribute inline 1
boehmes@52722
   354
    expr-attr
boehmes@52722
   355
      true
boehmes@52722
   356
fun-decl $dot 3 0
boehmes@52722
   357
    type-con $ptr 0
boehmes@52722
   358
    type-con $field 0
boehmes@52722
   359
    type-con $ptr 0
boehmes@52722
   360
fun-decl $emb 3 1
boehmes@52722
   361
    type-con $state 0
boehmes@52722
   362
    type-con $ptr 0
boehmes@52722
   363
    type-con $ptr 0
boehmes@52722
   364
  attribute inline 1
boehmes@52722
   365
    expr-attr
boehmes@52722
   366
      true
boehmes@52722
   367
fun-decl $path 3 1
boehmes@52722
   368
    type-con $state 0
boehmes@52722
   369
    type-con $ptr 0
boehmes@52722
   370
    type-con $field 0
boehmes@52722
   371
  attribute inline 1
boehmes@52722
   372
    expr-attr
boehmes@52722
   373
      true
boehmes@52722
   374
fun-decl $containing_struct 3 0
boehmes@52722
   375
    type-con $ptr 0
boehmes@52722
   376
    type-con $field 0
boehmes@52722
   377
    type-con $ptr 0
boehmes@52722
   378
fun-decl $containing_struct_ref 3 0
boehmes@52722
   379
    type-con $ptr 0
boehmes@52722
   380
    type-con $field 0
boehmes@52722
   381
    int
boehmes@52722
   382
fun-decl $is_primitive_non_volatile_field 2 0
boehmes@52722
   383
    type-con $field 0
boehmes@52722
   384
    bool
boehmes@52722
   385
fun-decl $is_primitive_volatile_field 2 0
boehmes@52722
   386
    type-con $field 0
boehmes@52722
   387
    bool
boehmes@52722
   388
fun-decl $is_primitive_embedded_array 3 0
boehmes@52722
   389
    type-con $field 0
boehmes@52722
   390
    int
boehmes@52722
   391
    bool
boehmes@52722
   392
fun-decl $is_primitive_embedded_volatile_array 4 0
boehmes@52722
   393
    type-con $field 0
boehmes@52722
   394
    int
boehmes@52722
   395
    type-con $ctype 0
boehmes@52722
   396
    bool
boehmes@52722
   397
fun-decl $static_field_properties 3 1
boehmes@52722
   398
    type-con $field 0
boehmes@52722
   399
    type-con $ctype 0
boehmes@52722
   400
    bool
boehmes@52722
   401
  attribute inline 1
boehmes@52722
   402
    expr-attr
boehmes@52722
   403
      true
boehmes@52722
   404
fun-decl $field_properties 6 1
boehmes@52722
   405
    type-con $state 0
boehmes@52722
   406
    type-con $ptr 0
boehmes@52722
   407
    type-con $field 0
boehmes@52722
   408
    type-con $ctype 0
boehmes@52722
   409
    bool
boehmes@52722
   410
    bool
boehmes@52722
   411
  attribute inline 1
boehmes@52722
   412
    expr-attr
boehmes@52722
   413
      true
boehmes@52722
   414
fun-decl $ts_typed 2 0
boehmes@52722
   415
    type-con $type_state 0
boehmes@52722
   416
    bool
boehmes@52722
   417
fun-decl $ts_emb 2 0
boehmes@52722
   418
    type-con $type_state 0
boehmes@52722
   419
    type-con $ptr 0
boehmes@52722
   420
fun-decl $ts_path 2 0
boehmes@52722
   421
    type-con $type_state 0
boehmes@52722
   422
    type-con $field 0
boehmes@52722
   423
fun-decl $ts_is_array_elt 2 0
boehmes@52722
   424
    type-con $type_state 0
boehmes@52722
   425
    bool
boehmes@52722
   426
fun-decl $ts_is_volatile 2 0
boehmes@52722
   427
    type-con $type_state 0
boehmes@52722
   428
    bool
boehmes@52722
   429
fun-decl $is_object_root 3 1
boehmes@52722
   430
    type-con $state 0
boehmes@52722
   431
    type-con $ptr 0
boehmes@52722
   432
    bool
boehmes@52722
   433
  attribute inline 1
boehmes@52722
   434
    expr-attr
boehmes@52722
   435
      true
boehmes@52722
   436
fun-decl $is_volatile 3 1
boehmes@52722
   437
    type-con $state 0
boehmes@52722
   438
    type-con $ptr 0
boehmes@52722
   439
    bool
boehmes@52722
   440
  attribute inline 1
boehmes@52722
   441
    expr-attr
boehmes@52722
   442
      true
boehmes@52722
   443
fun-decl $is_malloc_root 3 1
boehmes@52722
   444
    type-con $state 0
boehmes@52722
   445
    type-con $ptr 0
boehmes@52722
   446
    bool
boehmes@52722
   447
  attribute inline 1
boehmes@52722
   448
    expr-attr
boehmes@52722
   449
      true
boehmes@52722
   450
fun-decl $current_timestamp 2 0
boehmes@52722
   451
    type-con $state 0
boehmes@52722
   452
    int
boehmes@52722
   453
fun-decl $is_fresh 4 1
boehmes@52722
   454
    type-con $state 0
boehmes@52722
   455
    type-con $state 0
boehmes@52722
   456
    type-con $ptr 0
boehmes@52722
   457
    bool
boehmes@52722
   458
  attribute inline 1
boehmes@52722
   459
    expr-attr
boehmes@52722
   460
      true
boehmes@52722
   461
fun-decl $in_writes_at 3 0
boehmes@52722
   462
    int
boehmes@52722
   463
    type-con $ptr 0
boehmes@52722
   464
    bool
boehmes@52722
   465
fun-decl $writable 4 1
boehmes@52722
   466
    type-con $state 0
boehmes@52722
   467
    int
boehmes@52722
   468
    type-con $ptr 0
boehmes@52722
   469
    bool
boehmes@52722
   470
  attribute inline 1
boehmes@52722
   471
    expr-attr
boehmes@52722
   472
      true
boehmes@52722
   473
fun-decl $top_writable 4 1
boehmes@52722
   474
    type-con $state 0
boehmes@52722
   475
    int
boehmes@52722
   476
    type-con $ptr 0
boehmes@52722
   477
    bool
boehmes@52722
   478
  attribute inline 1
boehmes@52722
   479
    expr-attr
boehmes@52722
   480
      true
boehmes@52722
   481
fun-decl $struct_zero 1 0
boehmes@52722
   482
    type-con $struct 0
boehmes@52722
   483
fun-decl $vs_base 3 1
boehmes@52722
   484
    type-con $struct 0
boehmes@52722
   485
    type-con $ctype 0
boehmes@52722
   486
    type-con $ptr 0
boehmes@52722
   487
  attribute inline 1
boehmes@52722
   488
    expr-attr
boehmes@52722
   489
      true
boehmes@52722
   490
fun-decl $vs_base_ref 2 0
boehmes@52722
   491
    type-con $struct 0
boehmes@52722
   492
    int
boehmes@52722
   493
fun-decl $vs_state 2 0
boehmes@52722
   494
    type-con $struct 0
boehmes@52722
   495
    type-con $state 0
boehmes@52722
   496
fun-decl $vs_ctor 3 0
boehmes@52722
   497
    type-con $state 0
boehmes@52722
   498
    type-con $ptr 0
boehmes@52722
   499
    type-con $struct 0
boehmes@52722
   500
fun-decl $rec_zero 1 0
boehmes@52722
   501
    type-con $record 0
boehmes@52722
   502
fun-decl $rec_update 4 0
boehmes@52722
   503
    type-con $record 0
boehmes@52722
   504
    type-con $field 0
boehmes@52722
   505
    int
boehmes@52722
   506
    type-con $record 0
boehmes@52722
   507
fun-decl $rec_fetch 3 0
boehmes@52722
   508
    type-con $record 0
boehmes@52722
   509
    type-con $field 0
boehmes@52722
   510
    int
boehmes@52722
   511
fun-decl $rec_update_bv 7 0
boehmes@52722
   512
    type-con $record 0
boehmes@52722
   513
    type-con $field 0
boehmes@52722
   514
    int
boehmes@52722
   515
    int
boehmes@52722
   516
    int
boehmes@52722
   517
    int
boehmes@52722
   518
    type-con $record 0
boehmes@52722
   519
fun-decl $is_record_type 2 0
boehmes@52722
   520
    type-con $ctype 0
boehmes@52722
   521
    bool
boehmes@52722
   522
fun-decl $is_record_field 4 0
boehmes@52722
   523
    type-con $ctype 0
boehmes@52722
   524
    type-con $field 0
boehmes@52722
   525
    type-con $ctype 0
boehmes@52722
   526
    bool
boehmes@52722
   527
fun-decl $as_record_record_field 2 0
boehmes@52722
   528
    type-con $field 0
boehmes@52722
   529
    type-con $field 0
boehmes@52722
   530
fun-decl $rec_eq 3 0
boehmes@52722
   531
    type-con $record 0
boehmes@52722
   532
    type-con $record 0
boehmes@52722
   533
    bool
boehmes@52722
   534
fun-decl $rec_base_eq 3 0
boehmes@52722
   535
    int
boehmes@52722
   536
    int
boehmes@52722
   537
    bool
boehmes@52722
   538
fun-decl $int_to_record 2 0
boehmes@52722
   539
    int
boehmes@52722
   540
    type-con $record 0
boehmes@52722
   541
fun-decl $record_to_int 2 0
boehmes@52722
   542
    type-con $record 0
boehmes@52722
   543
    int
boehmes@52722
   544
fun-decl $good_state 2 0
boehmes@52722
   545
    type-con $state 0
boehmes@52722
   546
    bool
boehmes@52722
   547
fun-decl $invok_state 2 0
boehmes@52722
   548
    type-con $state 0
boehmes@52722
   549
    bool
boehmes@52722
   550
fun-decl $has_volatile_owns_set 2 0
boehmes@52722
   551
    type-con $ctype 0
boehmes@52722
   552
    bool
boehmes@52722
   553
fun-decl $owns_set_field 2 0
boehmes@52722
   554
    type-con $ctype 0
boehmes@52722
   555
    type-con $field 0
boehmes@52722
   556
fun-decl $st_owner 2 0
boehmes@52722
   557
    type-con $status 0
boehmes@52722
   558
    type-con $ptr 0
boehmes@52722
   559
fun-decl $st_closed 2 0
boehmes@52722
   560
    type-con $status 0
boehmes@52722
   561
    bool
boehmes@52722
   562
fun-decl $st_timestamp 2 0
boehmes@52722
   563
    type-con $status 0
boehmes@52722
   564
    int
boehmes@52722
   565
fun-decl $st_ref_cnt 2 0
boehmes@52722
   566
    type-con $status 0
boehmes@52722
   567
    int
boehmes@52722
   568
fun-decl $owner 3 0
boehmes@52722
   569
    type-con $state 0
boehmes@52722
   570
    type-con $ptr 0
boehmes@52722
   571
    type-con $ptr 0
boehmes@52722
   572
fun-decl $closed 3 0
boehmes@52722
   573
    type-con $state 0
boehmes@52722
   574
    type-con $ptr 0
boehmes@52722
   575
    bool
boehmes@52722
   576
fun-decl $timestamp 3 0
boehmes@52722
   577
    type-con $state 0
boehmes@52722
   578
    type-con $ptr 0
boehmes@52722
   579
    int
boehmes@52722
   580
fun-decl $position_marker 1 0
boehmes@52722
   581
    bool
boehmes@52722
   582
fun-decl $st 3 1
boehmes@52722
   583
    type-con $state 0
boehmes@52722
   584
    type-con $ptr 0
boehmes@52722
   585
    type-con $status 0
boehmes@52722
   586
  attribute inline 1
boehmes@52722
   587
    expr-attr
boehmes@52722
   588
      true
boehmes@52722
   589
fun-decl $ts 3 1
boehmes@52722
   590
    type-con $state 0
boehmes@52722
   591
    type-con $ptr 0
boehmes@52722
   592
    type-con $type_state 0
boehmes@52722
   593
  attribute inline 1
boehmes@52722
   594
    expr-attr
boehmes@52722
   595
      true
boehmes@52722
   596
fun-decl $owns 3 1
boehmes@52722
   597
    type-con $state 0
boehmes@52722
   598
    type-con $ptr 0
boehmes@52722
   599
    type-con $ptrset 0
boehmes@52722
   600
  attribute weight 1
boehmes@52722
   601
    expr-attr
boehmes@52722
   602
      int-num 0
boehmes@52722
   603
fun-decl $nested 3 1
boehmes@52722
   604
    type-con $state 0
boehmes@52722
   605
    type-con $ptr 0
boehmes@52722
   606
    bool
boehmes@52722
   607
  attribute inline 1
boehmes@52722
   608
    expr-attr
boehmes@52722
   609
      true
boehmes@52722
   610
fun-decl $nested_in 4 1
boehmes@52722
   611
    type-con $state 0
boehmes@52722
   612
    type-con $ptr 0
boehmes@52722
   613
    type-con $ptr 0
boehmes@52722
   614
    bool
boehmes@52722
   615
  attribute inline 1
boehmes@52722
   616
    expr-attr
boehmes@52722
   617
      true
boehmes@52722
   618
fun-decl $wrapped 4 1
boehmes@52722
   619
    type-con $state 0
boehmes@52722
   620
    type-con $ptr 0
boehmes@52722
   621
    type-con $ctype 0
boehmes@52722
   622
    bool
boehmes@52722
   623
  attribute inline 1
boehmes@52722
   624
    expr-attr
boehmes@52722
   625
      true
boehmes@52722
   626
fun-decl $irrelevant 3 1
boehmes@52722
   627
    type-con $state 0
boehmes@52722
   628
    type-con $ptr 0
boehmes@52722
   629
    bool
boehmes@52722
   630
  attribute inline 1
boehmes@52722
   631
    expr-attr
boehmes@52722
   632
      true
boehmes@52722
   633
fun-decl $mutable 3 1
boehmes@52722
   634
    type-con $state 0
boehmes@52722
   635
    type-con $ptr 0
boehmes@52722
   636
    bool
boehmes@52722
   637
  attribute weight 1
boehmes@52722
   638
    expr-attr
boehmes@52722
   639
      int-num 0
boehmes@52722
   640
fun-decl $thread_owned 3 1
boehmes@52722
   641
    type-con $state 0
boehmes@52722
   642
    type-con $ptr 0
boehmes@52722
   643
    bool
boehmes@52722
   644
  attribute inline 1
boehmes@52722
   645
    expr-attr
boehmes@52722
   646
      true
boehmes@52722
   647
fun-decl $thread_owned_or_even_mutable 3 1
boehmes@52722
   648
    type-con $state 0
boehmes@52722
   649
    type-con $ptr 0
boehmes@52722
   650
    bool
boehmes@52722
   651
  attribute inline 1
boehmes@52722
   652
    expr-attr
boehmes@52722
   653
      true
boehmes@52722
   654
fun-decl $typed 3 0
boehmes@52722
   655
    type-con $state 0
boehmes@52722
   656
    type-con $ptr 0
boehmes@52722
   657
    bool
boehmes@52722
   658
fun-decl $typed2 4 1
boehmes@52722
   659
    type-con $state 0
boehmes@52722
   660
    type-con $ptr 0
boehmes@52722
   661
    type-con $ctype 0
boehmes@52722
   662
    bool
boehmes@52722
   663
  attribute inline 1
boehmes@52722
   664
    expr-attr
boehmes@52722
   665
      true
boehmes@52722
   666
fun-decl $ptr_eq 3 1
boehmes@52722
   667
    type-con $ptr 0
boehmes@52722
   668
    type-con $ptr 0
boehmes@52722
   669
    bool
boehmes@52722
   670
  attribute inline 1
boehmes@52722
   671
    expr-attr
boehmes@52722
   672
      true
boehmes@52722
   673
fun-decl $ptr_neq 3 1
boehmes@52722
   674
    type-con $ptr 0
boehmes@52722
   675
    type-con $ptr 0
boehmes@52722
   676
    bool
boehmes@52722
   677
  attribute inline 1
boehmes@52722
   678
    expr-attr
boehmes@52722
   679
      true
boehmes@52722
   680
fun-decl $is_primitive_field_of 4 1
boehmes@52722
   681
    type-con $state 0
boehmes@52722
   682
    type-con $ptr 0
boehmes@52722
   683
    type-con $ptr 0
boehmes@52722
   684
    bool
boehmes@52722
   685
  attribute inline 1
boehmes@52722
   686
    expr-attr
boehmes@52722
   687
      true
boehmes@52722
   688
fun-decl $instantiate_st 2 0
boehmes@52722
   689
    type-con $status 0
boehmes@52722
   690
    bool
boehmes@52722
   691
fun-decl $is_domain_root 3 0
boehmes@52722
   692
    type-con $state 0
boehmes@52722
   693
    type-con $ptr 0
boehmes@52722
   694
    bool
boehmes@52722
   695
fun-decl $in_wrapped_domain 3 0
boehmes@52722
   696
    type-con $state 0
boehmes@52722
   697
    type-con $ptr 0
boehmes@52722
   698
    bool
boehmes@52722
   699
fun-decl $thread_local_np 3 1
boehmes@52722
   700
    type-con $state 0
boehmes@52722
   701
    type-con $ptr 0
boehmes@52722
   702
    bool
boehmes@52722
   703
  attribute inline 1
boehmes@52722
   704
    expr-attr
boehmes@52722
   705
      true
boehmes@52722
   706
fun-decl $thread_local 3 0
boehmes@52722
   707
    type-con $state 0
boehmes@52722
   708
    type-con $ptr 0
boehmes@52722
   709
    bool
boehmes@52722
   710
fun-decl $thread_local2 4 1
boehmes@52722
   711
    type-con $state 0
boehmes@52722
   712
    type-con $ptr 0
boehmes@52722
   713
    type-con $ctype 0
boehmes@52722
   714
    bool
boehmes@52722
   715
  attribute inline 1
boehmes@52722
   716
    expr-attr
boehmes@52722
   717
      true
boehmes@52722
   718
fun-decl $dont_instantiate 2 0
boehmes@52722
   719
    type-con $ptr 0
boehmes@52722
   720
    bool
boehmes@52722
   721
fun-decl $dont_instantiate_int 2 0
boehmes@52722
   722
    int
boehmes@52722
   723
    bool
boehmes@52722
   724
fun-decl $dont_instantiate_state 2 0
boehmes@52722
   725
    type-con $state 0
boehmes@52722
   726
    bool
boehmes@52722
   727
fun-decl $instantiate_int 2 0
boehmes@52722
   728
    int
boehmes@52722
   729
    bool
boehmes@52722
   730
fun-decl $instantiate_bool 2 0
boehmes@52722
   731
    bool
boehmes@52722
   732
    bool
boehmes@52722
   733
fun-decl $instantiate_ptr 2 0
boehmes@52722
   734
    type-con $ptr 0
boehmes@52722
   735
    bool
boehmes@52722
   736
fun-decl $instantiate_ptrset 2 0
boehmes@52722
   737
    type-con $ptrset 0
boehmes@52722
   738
    bool
boehmes@52722
   739
fun-decl $inv 4 1
boehmes@52722
   740
    type-con $state 0
boehmes@52722
   741
    type-con $ptr 0
boehmes@52722
   742
    type-con $ctype 0
boehmes@52722
   743
    bool
boehmes@52722
   744
  attribute inline 1
boehmes@52722
   745
    expr-attr
boehmes@52722
   746
      true
boehmes@52722
   747
fun-decl $inv2nt 4 1
boehmes@52722
   748
    type-con $state 0
boehmes@52722
   749
    type-con $state 0
boehmes@52722
   750
    type-con $ptr 0
boehmes@52722
   751
    bool
boehmes@52722
   752
  attribute inline 1
boehmes@52722
   753
    expr-attr
boehmes@52722
   754
      true
boehmes@52722
   755
fun-decl $imply_inv 4 0
boehmes@52722
   756
    type-con $state 0
boehmes@52722
   757
    type-con $ptr 0
boehmes@52722
   758
    type-con $ctype 0
boehmes@52722
   759
    bool
boehmes@52722
   760
fun-decl $inv2 5 0
boehmes@52722
   761
    type-con $state 0
boehmes@52722
   762
    type-con $state 0
boehmes@52722
   763
    type-con $ptr 0
boehmes@52722
   764
    type-con $ctype 0
boehmes@52722
   765
    bool
boehmes@52722
   766
fun-decl $inv2_when_closed 5 1
boehmes@52722
   767
    type-con $state 0
boehmes@52722
   768
    type-con $state 0
boehmes@52722
   769
    type-con $ptr 0
boehmes@52722
   770
    type-con $ctype 0
boehmes@52722
   771
    bool
boehmes@52722
   772
  attribute inline 1
boehmes@52722
   773
    expr-attr
boehmes@52722
   774
      true
boehmes@52722
   775
fun-decl $sequential 5 1
boehmes@52722
   776
    type-con $state 0
boehmes@52722
   777
    type-con $state 0
boehmes@52722
   778
    type-con $ptr 0
boehmes@52722
   779
    type-con $ctype 0
boehmes@52722
   780
    bool
boehmes@52722
   781
  attribute weight 1
boehmes@52722
   782
    expr-attr
boehmes@52722
   783
      int-num 0
boehmes@52722
   784
fun-decl $depends 5 1
boehmes@52722
   785
    type-con $state 0
boehmes@52722
   786
    type-con $state 0
boehmes@52722
   787
    type-con $ptr 0
boehmes@52722
   788
    type-con $ptr 0
boehmes@52722
   789
    bool
boehmes@52722
   790
  attribute weight 1
boehmes@52722
   791
    expr-attr
boehmes@52722
   792
      int-num 0
boehmes@52722
   793
fun-decl $spans_the_same 5 1
boehmes@52722
   794
    type-con $state 0
boehmes@52722
   795
    type-con $state 0
boehmes@52722
   796
    type-con $ptr 0
boehmes@52722
   797
    type-con $ctype 0
boehmes@52722
   798
    bool
boehmes@52722
   799
  attribute weight 1
boehmes@52722
   800
    expr-attr
boehmes@52722
   801
      int-num 0
boehmes@52722
   802
fun-decl $state_spans_the_same 5 0
boehmes@52722
   803
    type-con $state 0
boehmes@52722
   804
    type-con $state 0
boehmes@52722
   805
    type-con $ptr 0
boehmes@52722
   806
    type-con $ctype 0
boehmes@52722
   807
    bool
boehmes@52722
   808
fun-decl $nonvolatile_spans_the_same 5 1
boehmes@52722
   809
    type-con $state 0
boehmes@52722
   810
    type-con $state 0
boehmes@52722
   811
    type-con $ptr 0
boehmes@52722
   812
    type-con $ctype 0
boehmes@52722
   813
    bool
boehmes@52722
   814
  attribute weight 1
boehmes@52722
   815
    expr-attr
boehmes@52722
   816
      int-num 0
boehmes@52722
   817
fun-decl $state_nonvolatile_spans_the_same 5 0
boehmes@52722
   818
    type-con $state 0
boehmes@52722
   819
    type-con $state 0
boehmes@52722
   820
    type-con $ptr 0
boehmes@52722
   821
    type-con $ctype 0
boehmes@52722
   822
    bool
boehmes@52722
   823
fun-decl $in_extent_of 4 1
boehmes@52722
   824
    type-con $state 0
boehmes@52722
   825
    type-con $ptr 0
boehmes@52722
   826
    type-con $ptr 0
boehmes@52722
   827
    bool
boehmes@52722
   828
  attribute inline 1
boehmes@52722
   829
    expr-attr
boehmes@52722
   830
      true
boehmes@52722
   831
fun-decl $in_full_extent_of 3 1
boehmes@52722
   832
    type-con $ptr 0
boehmes@52722
   833
    type-con $ptr 0
boehmes@52722
   834
    bool
boehmes@52722
   835
  attribute inline 1
boehmes@52722
   836
    expr-attr
boehmes@52722
   837
      true
boehmes@52722
   838
fun-decl $extent_mutable 3 0
boehmes@52722
   839
    type-con $state 0
boehmes@52722
   840
    type-con $ptr 0
boehmes@52722
   841
    bool
boehmes@52722
   842
fun-decl $extent_is_fresh 4 0
boehmes@52722
   843
    type-con $state 0
boehmes@52722
   844
    type-con $state 0
boehmes@52722
   845
    type-con $ptr 0
boehmes@52722
   846
    bool
boehmes@52722
   847
fun-decl $forall_inv2_when_closed 3 1
boehmes@52722
   848
    type-con $state 0
boehmes@52722
   849
    type-con $state 0
boehmes@52722
   850
    bool
boehmes@52722
   851
  attribute inline 1
boehmes@52722
   852
    expr-attr
boehmes@52722
   853
      true
boehmes@52722
   854
fun-decl $function_entry 2 0
boehmes@52722
   855
    type-con $state 0
boehmes@52722
   856
    bool
boehmes@52722
   857
fun-decl $full_stop 2 0
boehmes@52722
   858
    type-con $state 0
boehmes@52722
   859
    bool
boehmes@52722
   860
fun-decl $full_stop_ext 3 1
boehmes@52722
   861
    type-con $token 0
boehmes@52722
   862
    type-con $state 0
boehmes@52722
   863
    bool
boehmes@52722
   864
  attribute inline 1
boehmes@52722
   865
    expr-attr
boehmes@52722
   866
      true
boehmes@52722
   867
fun-decl $file_name_is 3 0
boehmes@52722
   868
    int
boehmes@52722
   869
    type-con $token 0
boehmes@52722
   870
    bool
boehmes@52722
   871
fun-decl $closed_is_transitive 2 1
boehmes@52722
   872
    type-con $state 0
boehmes@52722
   873
    bool
boehmes@52722
   874
  attribute inline 1
boehmes@52722
   875
    expr-attr
boehmes@52722
   876
      true
boehmes@52722
   877
fun-decl $call_transition 3 0
boehmes@52722
   878
    type-con $state 0
boehmes@52722
   879
    type-con $state 0
boehmes@52722
   880
    bool
boehmes@52722
   881
fun-decl $good_state_ext 3 0
boehmes@52722
   882
    type-con $token 0
boehmes@52722
   883
    type-con $state 0
boehmes@52722
   884
    bool
boehmes@52722
   885
fun-decl $local_value_is 6 0
boehmes@52722
   886
    type-con $state 0
boehmes@52722
   887
    type-con $token 0
boehmes@52722
   888
    type-con $token 0
boehmes@52722
   889
    int
boehmes@52722
   890
    type-con $ctype 0
boehmes@52722
   891
    bool
boehmes@52722
   892
fun-decl $local_value_is_ptr 6 0
boehmes@52722
   893
    type-con $state 0
boehmes@52722
   894
    type-con $token 0
boehmes@52722
   895
    type-con $token 0
boehmes@52722
   896
    type-con $ptr 0
boehmes@52722
   897
    type-con $ctype 0
boehmes@52722
   898
    bool
boehmes@52722
   899
fun-decl $read_ptr_m 4 0
boehmes@52722
   900
    type-con $state 0
boehmes@52722
   901
    type-con $ptr 0
boehmes@52722
   902
    type-con $ctype 0
boehmes@52722
   903
    type-con $ptr 0
boehmes@52722
   904
fun-decl $type_code_is 3 0
boehmes@52722
   905
    int
boehmes@52722
   906
    type-con $ctype 0
boehmes@52722
   907
    bool
boehmes@52722
   908
fun-decl $function_arg_type 4 0
boehmes@52722
   909
    type-con $pure_function 0
boehmes@52722
   910
    int
boehmes@52722
   911
    type-con $ctype 0
boehmes@52722
   912
    bool
boehmes@52722
   913
fun-decl $ver_domain 2 0
boehmes@52722
   914
    type-con $version 0
boehmes@52722
   915
    type-con $ptrset 0
boehmes@52722
   916
fun-decl $read_version 3 1
boehmes@52722
   917
    type-con $state 0
boehmes@52722
   918
    type-con $ptr 0
boehmes@52722
   919
    type-con $version 0
boehmes@52722
   920
  attribute weight 1
boehmes@52722
   921
    expr-attr
boehmes@52722
   922
      int-num 0
boehmes@52722
   923
fun-decl $domain 3 1
boehmes@52722
   924
    type-con $state 0
boehmes@52722
   925
    type-con $ptr 0
boehmes@52722
   926
    type-con $ptrset 0
boehmes@52722
   927
  attribute weight 1
boehmes@52722
   928
    expr-attr
boehmes@52722
   929
      int-num 0
boehmes@52722
   930
fun-decl $in_domain 4 0
boehmes@52722
   931
    type-con $state 0
boehmes@52722
   932
    type-con $ptr 0
boehmes@52722
   933
    type-con $ptr 0
boehmes@52722
   934
    bool
boehmes@52722
   935
fun-decl $in_vdomain 4 0
boehmes@52722
   936
    type-con $state 0
boehmes@52722
   937
    type-con $ptr 0
boehmes@52722
   938
    type-con $ptr 0
boehmes@52722
   939
    bool
boehmes@52722
   940
fun-decl $in_domain_lab 5 0
boehmes@52722
   941
    type-con $state 0
boehmes@52722
   942
    type-con $ptr 0
boehmes@52722
   943
    type-con $ptr 0
boehmes@52722
   944
    type-con $label 0
boehmes@52722
   945
    bool
boehmes@52722
   946
fun-decl $in_vdomain_lab 5 0
boehmes@52722
   947
    type-con $state 0
boehmes@52722
   948
    type-con $ptr 0
boehmes@52722
   949
    type-con $ptr 0
boehmes@52722
   950
    type-con $label 0
boehmes@52722
   951
    bool
boehmes@52722
   952
fun-decl $inv_lab 4 0
boehmes@52722
   953
    type-con $state 0
boehmes@52722
   954
    type-con $ptr 0
boehmes@52722
   955
    type-con $label 0
boehmes@52722
   956
    bool
boehmes@52722
   957
fun-decl $dom_thread_local 3 1
boehmes@52722
   958
    type-con $state 0
boehmes@52722
   959
    type-con $ptr 0
boehmes@52722
   960
    bool
boehmes@52722
   961
  attribute inline 1
boehmes@52722
   962
    expr-attr
boehmes@52722
   963
      true
boehmes@52722
   964
fun-decl $fetch_from_domain 3 0
boehmes@52722
   965
    type-con $version 0
boehmes@52722
   966
    type-con $ptr 0
boehmes@52722
   967
    int
boehmes@52722
   968
fun-decl $in_claim_domain 3 0
boehmes@52722
   969
    type-con $ptr 0
boehmes@52722
   970
    type-con $ptr 0
boehmes@52722
   971
    bool
boehmes@52722
   972
fun-decl $by_claim 5 1
boehmes@52722
   973
    type-con $state 0
boehmes@52722
   974
    type-con $ptr 0
boehmes@52722
   975
    type-con $ptr 0
boehmes@52722
   976
    type-con $ptr 0
boehmes@52722
   977
    type-con $ptr 0
boehmes@52722
   978
  attribute weight 1
boehmes@52722
   979
    expr-attr
boehmes@52722
   980
      int-num 0
boehmes@52722
   981
fun-decl $claim_version 2 0
boehmes@52722
   982
    type-con $ptr 0
boehmes@52722
   983
    type-con $version 0
boehmes@52722
   984
fun-decl $read_vol_version 3 1
boehmes@52722
   985
    type-con $state 0
boehmes@52722
   986
    type-con $ptr 0
boehmes@52722
   987
    type-con $vol_version 0
boehmes@52722
   988
  attribute weight 1
boehmes@52722
   989
    expr-attr
boehmes@52722
   990
      int-num 0
boehmes@52722
   991
fun-decl $fetch_from_vv 3 0
boehmes@52722
   992
    type-con $vol_version 0
boehmes@52722
   993
    type-con $ptr 0
boehmes@52722
   994
    int
boehmes@52722
   995
fun-decl $fetch_vol_field 4 1
boehmes@52722
   996
    type-con $state 0
boehmes@52722
   997
    type-con $ptr 0
boehmes@52722
   998
    type-con $field 0
boehmes@52722
   999
    int
boehmes@52722
  1000
  attribute inline 1
boehmes@52722
  1001
    expr-attr
boehmes@52722
  1002
      true
boehmes@52722
  1003
fun-decl $is_approved_by 4 0
boehmes@52722
  1004
    type-con $ctype 0
boehmes@52722
  1005
    type-con $field 0
boehmes@52722
  1006
    type-con $field 0
boehmes@52722
  1007
    bool
boehmes@52722
  1008
fun-decl $inv_is_approved_by_ptr 6 1
boehmes@52722
  1009
    type-con $state 0
boehmes@52722
  1010
    type-con $state 0
boehmes@52722
  1011
    type-con $ptr 0
boehmes@52722
  1012
    type-con $ptr 0
boehmes@52722
  1013
    type-con $field 0
boehmes@52722
  1014
    bool
boehmes@52722
  1015
  attribute inline 1
boehmes@52722
  1016
    expr-attr
boehmes@52722
  1017
      true
boehmes@52722
  1018
fun-decl $inv_is_approved_by 6 1
boehmes@52722
  1019
    type-con $state 0
boehmes@52722
  1020
    type-con $state 0
boehmes@52722
  1021
    type-con $ptr 0
boehmes@52722
  1022
    type-con $field 0
boehmes@52722
  1023
    type-con $field 0
boehmes@52722
  1024
    bool
boehmes@52722
  1025
  attribute inline 1
boehmes@52722
  1026
    expr-attr
boehmes@52722
  1027
      true
boehmes@52722
  1028
fun-decl $is_owner_approved 3 0
boehmes@52722
  1029
    type-con $ctype 0
boehmes@52722
  1030
    type-con $field 0
boehmes@52722
  1031
    bool
boehmes@52722
  1032
fun-decl $inv_is_owner_approved 5 1
boehmes@52722
  1033
    type-con $state 0
boehmes@52722
  1034
    type-con $state 0
boehmes@52722
  1035
    type-con $ptr 0
boehmes@52722
  1036
    type-con $field 0
boehmes@52722
  1037
    bool
boehmes@52722
  1038
  attribute inline 1
boehmes@52722
  1039
    expr-attr
boehmes@52722
  1040
      true
boehmes@52722
  1041
fun-decl $good_for_admissibility 2 0
boehmes@52722
  1042
    type-con $state 0
boehmes@52722
  1043
    bool
boehmes@52722
  1044
fun-decl $good_for_post_admissibility 2 0
boehmes@52722
  1045
    type-con $state 0
boehmes@52722
  1046
    bool
boehmes@52722
  1047
fun-decl $stuttering_pre 3 1
boehmes@52722
  1048
    type-con $state 0
boehmes@52722
  1049
    type-con $ptr 0
boehmes@52722
  1050
    bool
boehmes@52722
  1051
  attribute inline 1
boehmes@52722
  1052
    expr-attr
boehmes@52722
  1053
      true
boehmes@52722
  1054
fun-decl $admissibility_pre 3 1
boehmes@52722
  1055
    type-con $state 0
boehmes@52722
  1056
    type-con $ptr 0
boehmes@52722
  1057
    bool
boehmes@52722
  1058
  attribute inline 1
boehmes@52722
  1059
    expr-attr
boehmes@52722
  1060
      true
boehmes@52722
  1061
fun-decl $mutable_increases 3 1
boehmes@52722
  1062
    type-con $state 0
boehmes@52722
  1063
    type-con $state 0
boehmes@52722
  1064
    bool
boehmes@52722
  1065
  attribute inline 1
boehmes@52722
  1066
    expr-attr
boehmes@52722
  1067
      true
boehmes@52722
  1068
fun-decl $meta_eq 3 1
boehmes@52722
  1069
    type-con $state 0
boehmes@52722
  1070
    type-con $state 0
boehmes@52722
  1071
    bool
boehmes@52722
  1072
  attribute inline 1
boehmes@52722
  1073
    expr-attr
boehmes@52722
  1074
      true
boehmes@52722
  1075
fun-decl $is_stuttering_check 1 0
boehmes@52722
  1076
    bool
boehmes@52722
  1077
fun-decl $is_unwrap_check 1 0
boehmes@52722
  1078
    bool
boehmes@52722
  1079
fun-decl $is_admissibility_check 1 1
boehmes@52722
  1080
    bool
boehmes@52722
  1081
  attribute inline 1
boehmes@52722
  1082
    expr-attr
boehmes@52722
  1083
      true
boehmes@52722
  1084
fun-decl $good_for_pre_can_unwrap 2 0
boehmes@52722
  1085
    type-con $state 0
boehmes@52722
  1086
    bool
boehmes@52722
  1087
fun-decl $good_for_post_can_unwrap 2 0
boehmes@52722
  1088
    type-con $state 0
boehmes@52722
  1089
    bool
boehmes@52722
  1090
fun-decl $unwrap_check_pre 3 1
boehmes@52722
  1091
    type-con $state 0
boehmes@52722
  1092
    type-con $ptr 0
boehmes@52722
  1093
    bool
boehmes@52722
  1094
  attribute inline 1
boehmes@52722
  1095
    expr-attr
boehmes@52722
  1096
      true
boehmes@52722
  1097
fun-decl $update_int 4 0
boehmes@52722
  1098
    type-con $state 0
boehmes@52722
  1099
    type-con $ptr 0
boehmes@52722
  1100
    int
boehmes@52722
  1101
    type-con $state 0
boehmes@52722
  1102
fun-decl $timestamp_is_now 3 1
boehmes@52722
  1103
    type-con $state 0
boehmes@52722
  1104
    type-con $ptr 0
boehmes@52722
  1105
    bool
boehmes@52722
  1106
  attribute inline 1
boehmes@52722
  1107
    expr-attr
boehmes@52722
  1108
      true
boehmes@52722
  1109
fun-decl $now_writable 3 1
boehmes@52722
  1110
    type-con $state 0
boehmes@52722
  1111
    type-con $ptr 0
boehmes@52722
  1112
    bool
boehmes@52722
  1113
  attribute inline 1
boehmes@52722
  1114
    expr-attr
boehmes@52722
  1115
      true
boehmes@52722
  1116
fun-decl $timestamp_post 3 1
boehmes@52722
  1117
    type-con $state 0
boehmes@52722
  1118
    type-con $state 0
boehmes@52722
  1119
    bool
boehmes@52722
  1120
  attribute inline 1
boehmes@52722
  1121
    expr-attr
boehmes@52722
  1122
      true
boehmes@52722
  1123
fun-decl $timestamp_post_strict 3 1
boehmes@52722
  1124
    type-con $state 0
boehmes@52722
  1125
    type-con $state 0
boehmes@52722
  1126
    bool
boehmes@52722
  1127
  attribute inline 1
boehmes@52722
  1128
    expr-attr
boehmes@52722
  1129
      true
boehmes@52722
  1130
fun-decl $pre_wrap 2 0
boehmes@52722
  1131
    type-con $state 0
boehmes@52722
  1132
    bool
boehmes@52722
  1133
fun-decl $pre_unwrap 2 0
boehmes@52722
  1134
    type-con $state 0
boehmes@52722
  1135
    bool
boehmes@52722
  1136
fun-decl $pre_static_wrap 2 0
boehmes@52722
  1137
    type-con $state 0
boehmes@52722
  1138
    bool
boehmes@52722
  1139
fun-decl $pre_static_unwrap 2 0
boehmes@52722
  1140
    type-con $state 0
boehmes@52722
  1141
    bool
boehmes@52722
  1142
fun-decl $unwrap_post 5 1
boehmes@52722
  1143
    type-con $state 0
boehmes@52722
  1144
    type-con $state 0
boehmes@52722
  1145
    type-con $ptr 0
boehmes@52722
  1146
    type-con $ptr 0
boehmes@52722
  1147
    bool
boehmes@52722
  1148
  attribute inline 1
boehmes@52722
  1149
    expr-attr
boehmes@52722
  1150
      true
boehmes@52722
  1151
fun-decl $unwrap_post_claimable 5 1
boehmes@52722
  1152
    type-con $state 0
boehmes@52722
  1153
    type-con $state 0
boehmes@52722
  1154
    type-con $ptr 0
boehmes@52722
  1155
    type-con $ptr 0
boehmes@52722
  1156
    bool
boehmes@52722
  1157
  attribute inline 1
boehmes@52722
  1158
    expr-attr
boehmes@52722
  1159
      true
boehmes@52722
  1160
fun-decl $keeps 4 2
boehmes@52722
  1161
    type-con $state 0
boehmes@52722
  1162
    type-con $ptr 0
boehmes@52722
  1163
    type-con $ptr 0
boehmes@52722
  1164
    bool
boehmes@52722
  1165
  attribute inline 1
boehmes@52722
  1166
    expr-attr
boehmes@52722
  1167
      true
boehmes@52722
  1168
  attribute expand 1
boehmes@52722
  1169
    expr-attr
boehmes@52722
  1170
      true
boehmes@52722
  1171
fun-decl $expect_unreachable 1 0
boehmes@52722
  1172
    bool
boehmes@52722
  1173
fun-decl $taken_over 4 0
boehmes@52722
  1174
    type-con $state 0
boehmes@52722
  1175
    type-con $ptr 0
boehmes@52722
  1176
    type-con $ptr 0
boehmes@52722
  1177
    type-con $status 0
boehmes@52722
  1178
fun-decl $take_over 4 0
boehmes@52722
  1179
    type-con $state 0
boehmes@52722
  1180
    type-con $ptr 0
boehmes@52722
  1181
    type-con $ptr 0
boehmes@52722
  1182
    type-con $state 0
boehmes@52722
  1183
fun-decl $released 4 0
boehmes@52722
  1184
    type-con $state 0
boehmes@52722
  1185
    type-con $ptr 0
boehmes@52722
  1186
    type-con $ptr 0
boehmes@52722
  1187
    type-con $status 0
boehmes@52722
  1188
fun-decl $release 5 0
boehmes@52722
  1189
    type-con $state 0
boehmes@52722
  1190
    type-con $state 0
boehmes@52722
  1191
    type-con $ptr 0
boehmes@52722
  1192
    type-con $ptr 0
boehmes@52722
  1193
    type-con $state 0
boehmes@52722
  1194
fun-decl $post_unwrap 3 0
boehmes@52722
  1195
    type-con $state 0
boehmes@52722
  1196
    type-con $state 0
boehmes@52722
  1197
    bool
boehmes@52722
  1198
fun-decl $new_ownees 4 1
boehmes@52722
  1199
    type-con $state 0
boehmes@52722
  1200
    type-con $ptr 0
boehmes@52722
  1201
    type-con $ptrset 0
boehmes@52722
  1202
    type-con $ptrset 0
boehmes@52722
  1203
  attribute inline 1
boehmes@52722
  1204
    expr-attr
boehmes@52722
  1205
      true
boehmes@52722
  1206
fun-decl $get_memory_allocator 1 0
boehmes@52722
  1207
    type-con $ptr 0
boehmes@52722
  1208
fun-decl $memory_allocator_type 1 1
boehmes@52722
  1209
    type-con $ctype 0
boehmes@52722
  1210
  attribute unique 0
boehmes@52722
  1211
fun-decl $memory_allocator_ref 1 0
boehmes@52722
  1212
    int
boehmes@52722
  1213
fun-decl $program_entry_point 2 0
boehmes@52722
  1214
    type-con $state 0
boehmes@52722
  1215
    bool
boehmes@52722
  1216
fun-decl $program_entry_point_ch 2 0
boehmes@52722
  1217
    type-con $state 0
boehmes@52722
  1218
    bool
boehmes@52722
  1219
fun-decl $is_global 3 1
boehmes@52722
  1220
    type-con $ptr 0
boehmes@52722
  1221
    type-con $ctype 0
boehmes@52722
  1222
    bool
boehmes@52722
  1223
  attribute inline 1
boehmes@52722
  1224
    expr-attr
boehmes@52722
  1225
      true
boehmes@52722
  1226
fun-decl $is_global_array 4 1
boehmes@52722
  1227
    type-con $ptr 0
boehmes@52722
  1228
    type-con $ctype 0
boehmes@52722
  1229
    int
boehmes@52722
  1230
    bool
boehmes@52722
  1231
  attribute inline 1
boehmes@52722
  1232
    expr-attr
boehmes@52722
  1233
      true
boehmes@52722
  1234
fun-decl $active_option 3 1
boehmes@52722
  1235
    type-con $state 0
boehmes@52722
  1236
    type-con $ptr 0
boehmes@52722
  1237
    type-con $field 0
boehmes@52722
  1238
  attribute inline 1
boehmes@52722
  1239
    expr-attr
boehmes@52722
  1240
      true
boehmes@52722
  1241
fun-decl $ts_active_option 2 0
boehmes@52722
  1242
    type-con $type_state 0
boehmes@52722
  1243
    type-con $field 0
boehmes@52722
  1244
fun-decl $union_active 4 1
boehmes@52722
  1245
    type-con $state 0
boehmes@52722
  1246
    type-con $ptr 0
boehmes@52722
  1247
    type-con $field 0
boehmes@52722
  1248
    bool
boehmes@52722
  1249
  attribute inline 1
boehmes@52722
  1250
    expr-attr
boehmes@52722
  1251
      true
boehmes@52722
  1252
fun-decl $is_union_field 3 0
boehmes@52722
  1253
    type-con $ctype 0
boehmes@52722
  1254
    type-con $field 0
boehmes@52722
  1255
    bool
boehmes@52722
  1256
fun-decl $union_havoced 4 1
boehmes@52722
  1257
    type-con $state 0
boehmes@52722
  1258
    type-con $state 0
boehmes@52722
  1259
    type-con $ptr 0
boehmes@52722
  1260
    bool
boehmes@52722
  1261
  attribute inline 1
boehmes@52722
  1262
    expr-attr
boehmes@52722
  1263
      true
boehmes@52722
  1264
fun-decl $full_extent 2 0
boehmes@52722
  1265
    type-con $ptr 0
boehmes@52722
  1266
    type-con $ptrset 0
boehmes@52722
  1267
fun-decl $extent 3 0
boehmes@52722
  1268
    type-con $state 0
boehmes@52722
  1269
    type-con $ptr 0
boehmes@52722
  1270
    type-con $ptrset 0
boehmes@52722
  1271
fun-decl $span 2 0
boehmes@52722
  1272
    type-con $ptr 0
boehmes@52722
  1273
    type-con $ptrset 0
boehmes@52722
  1274
fun-decl $in_span_of 3 1
boehmes@52722
  1275
    type-con $ptr 0
boehmes@52722
  1276
    type-con $ptr 0
boehmes@52722
  1277
    bool
boehmes@52722
  1278
  attribute inline 1
boehmes@52722
  1279
    expr-attr
boehmes@52722
  1280
      true
boehmes@52722
  1281
fun-decl $first_option_typed 3 0
boehmes@52722
  1282
    type-con $state 0
boehmes@52722
  1283
    type-con $ptr 0
boehmes@52722
  1284
    bool
boehmes@52722
  1285
fun-decl $struct_extent 2 1
boehmes@52722
  1286
    type-con $ptr 0
boehmes@52722
  1287
    type-con $ptrset 0
boehmes@52722
  1288
  attribute inline 1
boehmes@52722
  1289
    expr-attr
boehmes@52722
  1290
      true
boehmes@52722
  1291
fun-decl $in_struct_extent_of 3 1
boehmes@52722
  1292
    type-con $ptr 0
boehmes@52722
  1293
    type-con $ptr 0
boehmes@52722
  1294
    bool
boehmes@52722
  1295
  attribute inline 1
boehmes@52722
  1296
    expr-attr
boehmes@52722
  1297
      true
boehmes@52722
  1298
fun-decl $volatile_span 3 0
boehmes@52722
  1299
    type-con $state 0
boehmes@52722
  1300
    type-con $ptr 0
boehmes@52722
  1301
    type-con $ptrset 0
boehmes@52722
  1302
fun-decl $left_split 3 0
boehmes@52722
  1303
    type-con $ptr 0
boehmes@52722
  1304
    int
boehmes@52722
  1305
    type-con $ptr 0
boehmes@52722
  1306
fun-decl $right_split 3 0
boehmes@52722
  1307
    type-con $ptr 0
boehmes@52722
  1308
    int
boehmes@52722
  1309
    type-con $ptr 0
boehmes@52722
  1310
fun-decl $joined_array 3 0
boehmes@52722
  1311
    type-con $ptr 0
boehmes@52722
  1312
    type-con $ptr 0
boehmes@52722
  1313
    type-con $ptr 0
boehmes@52722
  1314
fun-decl $mutable_root 3 1
boehmes@52722
  1315
    type-con $state 0
boehmes@52722
  1316
    type-con $ptr 0
boehmes@52722
  1317
    bool
boehmes@52722
  1318
  attribute inline 1
boehmes@52722
  1319
    expr-attr
boehmes@52722
  1320
      true
boehmes@52722
  1321
fun-decl $set_in 3 0
boehmes@52722
  1322
    type-con $ptr 0
boehmes@52722
  1323
    type-con $ptrset 0
boehmes@52722
  1324
    bool
boehmes@52722
  1325
fun-decl $set_empty 1 0
boehmes@52722
  1326
    type-con $ptrset 0
boehmes@52722
  1327
fun-decl $set_singleton 2 0
boehmes@52722
  1328
    type-con $ptr 0
boehmes@52722
  1329
    type-con $ptrset 0
boehmes@52722
  1330
fun-decl $non_null_set_singleton 2 0
boehmes@52722
  1331
    type-con $ptr 0
boehmes@52722
  1332
    type-con $ptrset 0
boehmes@52722
  1333
fun-decl $set_union 3 0
boehmes@52722
  1334
    type-con $ptrset 0
boehmes@52722
  1335
    type-con $ptrset 0
boehmes@52722
  1336
    type-con $ptrset 0
boehmes@52722
  1337
fun-decl $set_difference 3 0
boehmes@52722
  1338
    type-con $ptrset 0
boehmes@52722
  1339
    type-con $ptrset 0
boehmes@52722
  1340
    type-con $ptrset 0
boehmes@52722
  1341
fun-decl $set_intersection 3 0
boehmes@52722
  1342
    type-con $ptrset 0
boehmes@52722
  1343
    type-con $ptrset 0
boehmes@52722
  1344
    type-con $ptrset 0
boehmes@52722
  1345
fun-decl $set_subset 3 0
boehmes@52722
  1346
    type-con $ptrset 0
boehmes@52722
  1347
    type-con $ptrset 0
boehmes@52722
  1348
    bool
boehmes@52722
  1349
fun-decl $set_eq 3 0
boehmes@52722
  1350
    type-con $ptrset 0
boehmes@52722
  1351
    type-con $ptrset 0
boehmes@52722
  1352
    bool
boehmes@52722
  1353
fun-decl $set_cardinality 2 0
boehmes@52722
  1354
    type-con $ptrset 0
boehmes@52722
  1355
    int
boehmes@52722
  1356
fun-decl $set_universe 1 0
boehmes@52722
  1357
    type-con $ptrset 0
boehmes@52722
  1358
fun-decl $set_disjoint 3 0
boehmes@52722
  1359
    type-con $ptrset 0
boehmes@52722
  1360
    type-con $ptrset 0
boehmes@52722
  1361
    bool
boehmes@52722
  1362
fun-decl $id_set_disjoint 4 0
boehmes@52722
  1363
    type-con $ptr 0
boehmes@52722
  1364
    type-con $ptrset 0
boehmes@52722
  1365
    type-con $ptrset 0
boehmes@52722
  1366
    int
boehmes@52722
  1367
fun-decl $set_in3 3 0
boehmes@52722
  1368
    type-con $ptr 0
boehmes@52722
  1369
    type-con $ptrset 0
boehmes@52722
  1370
    bool
boehmes@52722
  1371
fun-decl $set_in2 3 0
boehmes@52722
  1372
    type-con $ptr 0
boehmes@52722
  1373
    type-con $ptrset 0
boehmes@52722
  1374
    bool
boehmes@52722
  1375
fun-decl $in_some_owns 2 0
boehmes@52722
  1376
    type-con $ptr 0
boehmes@52722
  1377
    bool
boehmes@52722
  1378
fun-decl $set_in0 3 0
boehmes@52722
  1379
    type-con $ptr 0
boehmes@52722
  1380
    type-con $ptrset 0
boehmes@52722
  1381
    bool
boehmes@52722
  1382
fun-decl sk_hack 2 0
boehmes@52722
  1383
    bool
boehmes@52722
  1384
    bool
boehmes@52722
  1385
fun-decl $writes_nothing 3 1
boehmes@52722
  1386
    type-con $state 0
boehmes@52722
  1387
    type-con $state 0
boehmes@52722
  1388
    bool
boehmes@52722
  1389
  attribute inline 1
boehmes@52722
  1390
    expr-attr
boehmes@52722
  1391
      true
boehmes@52722
  1392
fun-decl $array 3 0
boehmes@52722
  1393
    type-con $ctype 0
boehmes@52722
  1394
    int
boehmes@52722
  1395
    type-con $ctype 0
boehmes@52722
  1396
fun-decl $element_type 2 0
boehmes@52722
  1397
    type-con $ctype 0
boehmes@52722
  1398
    type-con $ctype 0
boehmes@52722
  1399
fun-decl $array_length 2 0
boehmes@52722
  1400
    type-con $ctype 0
boehmes@52722
  1401
    int
boehmes@52722
  1402
fun-decl $is_array_elt 3 1
boehmes@52722
  1403
    type-con $state 0
boehmes@52722
  1404
    type-con $ptr 0
boehmes@52722
  1405
    bool
boehmes@52722
  1406
  attribute inline 1
boehmes@52722
  1407
    expr-attr
boehmes@52722
  1408
      true
boehmes@52722
  1409
fun-decl $inlined_array 3 1
boehmes@52722
  1410
    type-con $ptr 0
boehmes@52722
  1411
    type-con $ctype 0
boehmes@52722
  1412
    type-con $ptr 0
boehmes@52722
  1413
  attribute weight 1
boehmes@52722
  1414
    expr-attr
boehmes@52722
  1415
      int-num 0
boehmes@52722
  1416
fun-decl $idx 4 0
boehmes@52722
  1417
    type-con $ptr 0
boehmes@52722
  1418
    int
boehmes@52722
  1419
    type-con $ctype 0
boehmes@52722
  1420
    type-con $ptr 0
boehmes@52722
  1421
fun-decl $add.mul 4 2
boehmes@52722
  1422
    int
boehmes@52722
  1423
    int
boehmes@52722
  1424
    int
boehmes@52722
  1425
    int
boehmes@52722
  1426
  attribute inline 1
boehmes@52722
  1427
    expr-attr
boehmes@52722
  1428
      true
boehmes@52722
  1429
  attribute expand 1
boehmes@52722
  1430
    expr-attr
boehmes@52722
  1431
      true
boehmes@52722
  1432
fun-decl $add 3 2
boehmes@52722
  1433
    int
boehmes@52722
  1434
    int
boehmes@52722
  1435
    int
boehmes@52722
  1436
  attribute inline 1
boehmes@52722
  1437
    expr-attr
boehmes@52722
  1438
      true
boehmes@52722
  1439
  attribute expand 1
boehmes@52722
  1440
    expr-attr
boehmes@52722
  1441
      true
boehmes@52722
  1442
fun-decl $is_array_vol_or_nonvol 6 1
boehmes@52722
  1443
    type-con $state 0
boehmes@52722
  1444
    type-con $ptr 0
boehmes@52722
  1445
    type-con $ctype 0
boehmes@52722
  1446
    int
boehmes@52722
  1447
    bool
boehmes@52722
  1448
    bool
boehmes@52722
  1449
  attribute weight 1
boehmes@52722
  1450
    expr-attr
boehmes@52722
  1451
      int-num 0
boehmes@52722
  1452
fun-decl $is_array 5 1
boehmes@52722
  1453
    type-con $state 0
boehmes@52722
  1454
    type-con $ptr 0
boehmes@52722
  1455
    type-con $ctype 0
boehmes@52722
  1456
    int
boehmes@52722
  1457
    bool
boehmes@52722
  1458
  attribute weight 1
boehmes@52722
  1459
    expr-attr
boehmes@52722
  1460
      int-num 0
boehmes@52722
  1461
fun-decl $is_thread_local_array 5 1
boehmes@52722
  1462
    type-con $state 0
boehmes@52722
  1463
    type-con $ptr 0
boehmes@52722
  1464
    type-con $ctype 0
boehmes@52722
  1465
    int
boehmes@52722
  1466
    bool
boehmes@52722
  1467
  attribute inline 1
boehmes@52722
  1468
    expr-attr
boehmes@52722
  1469
      true
boehmes@52722
  1470
fun-decl $is_mutable_array 5 1
boehmes@52722
  1471
    type-con $state 0
boehmes@52722
  1472
    type-con $ptr 0
boehmes@52722
  1473
    type-con $ctype 0
boehmes@52722
  1474
    int
boehmes@52722
  1475
    bool
boehmes@52722
  1476
  attribute inline 1
boehmes@52722
  1477
    expr-attr
boehmes@52722
  1478
      true
boehmes@52722
  1479
fun-decl $is_array_emb 6 1
boehmes@52722
  1480
    type-con $state 0
boehmes@52722
  1481
    type-con $ptr 0
boehmes@52722
  1482
    type-con $ctype 0
boehmes@52722
  1483
    int
boehmes@52722
  1484
    type-con $ptr 0
boehmes@52722
  1485
    bool
boehmes@52722
  1486
  attribute inline 1
boehmes@52722
  1487
    expr-attr
boehmes@52722
  1488
      true
boehmes@52722
  1489
fun-decl $is_array_emb_path 8 1
boehmes@52722
  1490
    type-con $state 0
boehmes@52722
  1491
    type-con $ptr 0
boehmes@52722
  1492
    type-con $ctype 0
boehmes@52722
  1493
    int
boehmes@52722
  1494
    type-con $ptr 0
boehmes@52722
  1495
    type-con $field 0
boehmes@52722
  1496
    bool
boehmes@52722
  1497
    bool
boehmes@52722
  1498
  attribute inline 1
boehmes@52722
  1499
    expr-attr
boehmes@52722
  1500
      true
boehmes@52722
  1501
fun-decl $array_field_properties 6 1
boehmes@52722
  1502
    type-con $field 0
boehmes@52722
  1503
    type-con $ctype 0
boehmes@52722
  1504
    int
boehmes@52722
  1505
    bool
boehmes@52722
  1506
    bool
boehmes@52722
  1507
    bool
boehmes@52722
  1508
  attribute inline 1
boehmes@52722
  1509
    expr-attr
boehmes@52722
  1510
      true
boehmes@52722
  1511
fun-decl $no_inline_array_field_properties 6 1
boehmes@52722
  1512
    type-con $field 0
boehmes@52722
  1513
    type-con $ctype 0
boehmes@52722
  1514
    int
boehmes@52722
  1515
    bool
boehmes@52722
  1516
    bool
boehmes@52722
  1517
    bool
boehmes@52722
  1518
  attribute inline 1
boehmes@52722
  1519
    expr-attr
boehmes@52722
  1520
      true
boehmes@52722
  1521
fun-decl $array_elt_emb 4 1
boehmes@52722
  1522
    type-con $state 0
boehmes@52722
  1523
    type-con $ptr 0
boehmes@52722
  1524
    type-con $ptr 0
boehmes@52722
  1525
    bool
boehmes@52722
  1526
  attribute inline 1
boehmes@52722
  1527
    expr-attr
boehmes@52722
  1528
      true
boehmes@52722
  1529
fun-decl $array_members 4 0
boehmes@52722
  1530
    type-con $ptr 0
boehmes@52722
  1531
    type-con $ctype 0
boehmes@52722
  1532
    int
boehmes@52722
  1533
    type-con $ptrset 0
boehmes@52722
  1534
fun-decl $array_range 4 0
boehmes@52722
  1535
    type-con $ptr 0
boehmes@52722
  1536
    type-con $ctype 0
boehmes@52722
  1537
    int
boehmes@52722
  1538
    type-con $ptrset 0
boehmes@52722
  1539
fun-decl $non_null_array_range 4 0
boehmes@52722
  1540
    type-con $ptr 0
boehmes@52722
  1541
    type-con $ctype 0
boehmes@52722
  1542
    int
boehmes@52722
  1543
    type-con $ptrset 0
boehmes@52722
  1544
fun-decl $non_null_extent 3 0
boehmes@52722
  1545
    type-con $state 0
boehmes@52722
  1546
    type-con $ptr 0
boehmes@52722
  1547
    type-con $ptrset 0
boehmes@52722
  1548
fun-decl $as_array 4 1
boehmes@52722
  1549
    type-con $ptr 0
boehmes@52722
  1550
    type-con $ctype 0
boehmes@52722
  1551
    int
boehmes@52722
  1552
    type-con $ptr 0
boehmes@52722
  1553
  attribute inline 1
boehmes@52722
  1554
    expr-attr
boehmes@52722
  1555
      true
boehmes@52722
  1556
fun-decl $array_eq 6 1
boehmes@52722
  1557
    type-con $state 0
boehmes@52722
  1558
    type-con $state 0
boehmes@52722
  1559
    type-con $ptr 0
boehmes@52722
  1560
    type-con $ctype 0
boehmes@52722
  1561
    int
boehmes@52722
  1562
    bool
boehmes@52722
  1563
  attribute inline 1
boehmes@52722
  1564
    expr-attr
boehmes@52722
  1565
      true
boehmes@52722
  1566
fun-decl $index_within 3 0
boehmes@52722
  1567
    type-con $ptr 0
boehmes@52722
  1568
    type-con $ptr 0
boehmes@52722
  1569
    int
boehmes@52722
  1570
fun-decl $in_array 5 1
boehmes@52722
  1571
    type-con $ptr 0
boehmes@52722
  1572
    type-con $ptr 0
boehmes@52722
  1573
    type-con $ctype 0
boehmes@52722
  1574
    int
boehmes@52722
  1575
    bool
boehmes@52722
  1576
  attribute inline 1
boehmes@52722
  1577
    expr-attr
boehmes@52722
  1578
      true
boehmes@52722
  1579
fun-decl $in_array_full_extent_of 5 1
boehmes@52722
  1580
    type-con $ptr 0
boehmes@52722
  1581
    type-con $ptr 0
boehmes@52722
  1582
    type-con $ctype 0
boehmes@52722
  1583
    int
boehmes@52722
  1584
    bool
boehmes@52722
  1585
  attribute inline 1
boehmes@52722
  1586
    expr-attr
boehmes@52722
  1587
      true
boehmes@52722
  1588
fun-decl $in_array_extent_of 6 1
boehmes@52722
  1589
    type-con $state 0
boehmes@52722
  1590
    type-con $ptr 0
boehmes@52722
  1591
    type-con $ptr 0
boehmes@52722
  1592
    type-con $ctype 0
boehmes@52722
  1593
    int
boehmes@52722
  1594
    bool
boehmes@52722
  1595
  attribute inline 1
boehmes@52722
  1596
    expr-attr
boehmes@52722
  1597
      true
boehmes@52722
  1598
fun-decl $in_range 4 1
boehmes@52722
  1599
    int
boehmes@52722
  1600
    int
boehmes@52722
  1601
    int
boehmes@52722
  1602
    bool
boehmes@52722
  1603
  attribute inline 1
boehmes@52722
  1604
    expr-attr
boehmes@52722
  1605
      true
boehmes@52722
  1606
fun-decl $bool_to_int 2 1
boehmes@52722
  1607
    bool
boehmes@52722
  1608
    int
boehmes@52722
  1609
  attribute inline 1
boehmes@52722
  1610
    expr-attr
boehmes@52722
  1611
      true
boehmes@52722
  1612
fun-decl $int_to_bool 2 1
boehmes@52722
  1613
    int
boehmes@52722
  1614
    bool
boehmes@52722
  1615
  attribute inline 1
boehmes@52722
  1616
    expr-attr
boehmes@52722
  1617
      true
boehmes@52722
  1618
fun-decl $read_bool 3 1
boehmes@52722
  1619
    type-con $state 0
boehmes@52722
  1620
    type-con $ptr 0
boehmes@52722
  1621
    bool
boehmes@52722
  1622
  attribute inline 1
boehmes@52722
  1623
    expr-attr
boehmes@52722
  1624
      true
boehmes@52722
  1625
fun-decl $ite.int 4 3
boehmes@52722
  1626
    bool
boehmes@52722
  1627
    int
boehmes@52722
  1628
    int
boehmes@52722
  1629
    int
boehmes@52722
  1630
  attribute external 1
boehmes@52722
  1631
    string-attr ITE
boehmes@52722
  1632
  attribute bvz 1
boehmes@52722
  1633
    string-attr ITE
boehmes@52722
  1634
  attribute bvint 1
boehmes@52722
  1635
    string-attr ITE
boehmes@52722
  1636
fun-decl $ite.bool 4 3
boehmes@52722
  1637
    bool
boehmes@52722
  1638
    bool
boehmes@52722
  1639
    bool
boehmes@52722
  1640
    bool
boehmes@52722
  1641
  attribute external 1
boehmes@52722
  1642
    string-attr ITE
boehmes@52722
  1643
  attribute bvz 1
boehmes@52722
  1644
    string-attr ITE
boehmes@52722
  1645
  attribute bvint 1
boehmes@52722
  1646
    string-attr ITE
boehmes@52722
  1647
fun-decl $ite.ptr 4 3
boehmes@52722
  1648
    bool
boehmes@52722
  1649
    type-con $ptr 0
boehmes@52722
  1650
    type-con $ptr 0
boehmes@52722
  1651
    type-con $ptr 0
boehmes@52722
  1652
  attribute external 1
boehmes@52722
  1653
    string-attr ITE
boehmes@52722
  1654
  attribute bvz 1
boehmes@52722
  1655
    string-attr ITE
boehmes@52722
  1656
  attribute bvint 1
boehmes@52722
  1657
    string-attr ITE
boehmes@52722
  1658
fun-decl $ite.struct 4 3
boehmes@52722
  1659
    bool
boehmes@52722
  1660
    type-con $struct 0
boehmes@52722
  1661
    type-con $struct 0
boehmes@52722
  1662
    type-con $struct 0
boehmes@52722
  1663
  attribute external 1
boehmes@52722
  1664
    string-attr ITE
boehmes@52722
  1665
  attribute bvz 1
boehmes@52722
  1666
    string-attr ITE
boehmes@52722
  1667
  attribute bvint 1
boehmes@52722
  1668
    string-attr ITE
boehmes@52722
  1669
fun-decl $ite.ptrset 4 3
boehmes@52722
  1670
    bool
boehmes@52722
  1671
    type-con $ptrset 0
boehmes@52722
  1672
    type-con $ptrset 0
boehmes@52722
  1673
    type-con $ptrset 0
boehmes@52722
  1674
  attribute external 1
boehmes@52722
  1675
    string-attr ITE
boehmes@52722
  1676
  attribute bvz 1
boehmes@52722
  1677
    string-attr ITE
boehmes@52722
  1678
  attribute bvint 1
boehmes@52722
  1679
    string-attr ITE
boehmes@52722
  1680
fun-decl $ite.primitive 4 3
boehmes@52722
  1681
    bool
boehmes@52722
  1682
    type-con $primitive 0
boehmes@52722
  1683
    type-con $primitive 0
boehmes@52722
  1684
    type-con $primitive 0
boehmes@52722
  1685
  attribute external 1
boehmes@52722
  1686
    string-attr ITE
boehmes@52722
  1687
  attribute bvz 1
boehmes@52722
  1688
    string-attr ITE
boehmes@52722
  1689
  attribute bvint 1
boehmes@52722
  1690
    string-attr ITE
boehmes@52722
  1691
fun-decl $ite.record 4 3
boehmes@52722
  1692
    bool
boehmes@52722
  1693
    type-con $record 0
boehmes@52722
  1694
    type-con $record 0
boehmes@52722
  1695
    type-con $record 0
boehmes@52722
  1696
  attribute external 1
boehmes@52722
  1697
    string-attr ITE
boehmes@52722
  1698
  attribute bvz 1
boehmes@52722
  1699
    string-attr ITE
boehmes@52722
  1700
  attribute bvint 1
boehmes@52722
  1701
    string-attr ITE
boehmes@52722
  1702
fun-decl $bool_id 2 1
boehmes@52722
  1703
    bool
boehmes@52722
  1704
    bool
boehmes@52722
  1705
  attribute weight 1
boehmes@52722
  1706
    expr-attr
boehmes@52722
  1707
      int-num 0
boehmes@52722
  1708
fun-decl $min.i1 1 0
boehmes@52722
  1709
    int
boehmes@52722
  1710
fun-decl $max.i1 1 0
boehmes@52722
  1711
    int
boehmes@52722
  1712
fun-decl $min.i2 1 0
boehmes@52722
  1713
    int
boehmes@52722
  1714
fun-decl $max.i2 1 0
boehmes@52722
  1715
    int
boehmes@52722
  1716
fun-decl $min.i4 1 0
boehmes@52722
  1717
    int
boehmes@52722
  1718
fun-decl $max.i4 1 0
boehmes@52722
  1719
    int
boehmes@52722
  1720
fun-decl $min.i8 1 0
boehmes@52722
  1721
    int
boehmes@52722
  1722
fun-decl $max.i8 1 0
boehmes@52722
  1723
    int
boehmes@52722
  1724
fun-decl $max.u1 1 0
boehmes@52722
  1725
    int
boehmes@52722
  1726
fun-decl $max.u2 1 0
boehmes@52722
  1727
    int
boehmes@52722
  1728
fun-decl $max.u4 1 0
boehmes@52722
  1729
    int
boehmes@52722
  1730
fun-decl $max.u8 1 0
boehmes@52722
  1731
    int
boehmes@52722
  1732
fun-decl $in_range_i1 2 1
boehmes@52722
  1733
    int
boehmes@52722
  1734
    bool
boehmes@52722
  1735
  attribute inline 1
boehmes@52722
  1736
    expr-attr
boehmes@52722
  1737
      true
boehmes@52722
  1738
fun-decl $in_range_i2 2 1
boehmes@52722
  1739
    int
boehmes@52722
  1740
    bool
boehmes@52722
  1741
  attribute inline 1
boehmes@52722
  1742
    expr-attr
boehmes@52722
  1743
      true
boehmes@52722
  1744
fun-decl $in_range_i4 2 1
boehmes@52722
  1745
    int
boehmes@52722
  1746
    bool
boehmes@52722
  1747
  attribute inline 1
boehmes@52722
  1748
    expr-attr
boehmes@52722
  1749
      true
boehmes@52722
  1750
fun-decl $in_range_i8 2 1
boehmes@52722
  1751
    int
boehmes@52722
  1752
    bool
boehmes@52722
  1753
  attribute inline 1
boehmes@52722
  1754
    expr-attr
boehmes@52722
  1755
      true
boehmes@52722
  1756
fun-decl $in_range_u1 2 1
boehmes@52722
  1757
    int
boehmes@52722
  1758
    bool
boehmes@52722
  1759
  attribute inline 1
boehmes@52722
  1760
    expr-attr
boehmes@52722
  1761
      true
boehmes@52722
  1762
fun-decl $in_range_u2 2 1
boehmes@52722
  1763
    int
boehmes@52722
  1764
    bool
boehmes@52722
  1765
  attribute inline 1
boehmes@52722
  1766
    expr-attr
boehmes@52722
  1767
      true
boehmes@52722
  1768
fun-decl $in_range_u4 2 1
boehmes@52722
  1769
    int
boehmes@52722
  1770
    bool
boehmes@52722
  1771
  attribute inline 1
boehmes@52722
  1772
    expr-attr
boehmes@52722
  1773
      true
boehmes@52722
  1774
fun-decl $in_range_u8 2 1
boehmes@52722
  1775
    int
boehmes@52722
  1776
    bool
boehmes@52722
  1777
  attribute inline 1
boehmes@52722
  1778
    expr-attr
boehmes@52722
  1779
      true
boehmes@52722
  1780
fun-decl $in_range_div_i1 3 1
boehmes@52722
  1781
    int
boehmes@52722
  1782
    int
boehmes@52722
  1783
    bool
boehmes@52722
  1784
  attribute inline 1
boehmes@52722
  1785
    expr-attr
boehmes@52722
  1786
      true
boehmes@52722
  1787
fun-decl $in_range_div_i2 3 1
boehmes@52722
  1788
    int
boehmes@52722
  1789
    int
boehmes@52722
  1790
    bool
boehmes@52722
  1791
  attribute inline 1
boehmes@52722
  1792
    expr-attr
boehmes@52722
  1793
      true
boehmes@52722
  1794
fun-decl $in_range_div_i4 3 1
boehmes@52722
  1795
    int
boehmes@52722
  1796
    int
boehmes@52722
  1797
    bool
boehmes@52722
  1798
  attribute inline 1
boehmes@52722
  1799
    expr-attr
boehmes@52722
  1800
      true
boehmes@52722
  1801
fun-decl $in_range_div_i8 3 1
boehmes@52722
  1802
    int
boehmes@52722
  1803
    int
boehmes@52722
  1804
    bool
boehmes@52722
  1805
  attribute inline 1
boehmes@52722
  1806
    expr-attr
boehmes@52722
  1807
      true
boehmes@52722
  1808
fun-decl $read_i1 3 1
boehmes@52722
  1809
    type-con $state 0
boehmes@52722
  1810
    type-con $ptr 0
boehmes@52722
  1811
    int
boehmes@52722
  1812
  attribute weight 1
boehmes@52722
  1813
    expr-attr
boehmes@52722
  1814
      int-num 0
boehmes@52722
  1815
fun-decl $read_i2 3 1
boehmes@52722
  1816
    type-con $state 0
boehmes@52722
  1817
    type-con $ptr 0
boehmes@52722
  1818
    int
boehmes@52722
  1819
  attribute weight 1
boehmes@52722
  1820
    expr-attr
boehmes@52722
  1821
      int-num 0
boehmes@52722
  1822
fun-decl $read_i4 3 1
boehmes@52722
  1823
    type-con $state 0
boehmes@52722
  1824
    type-con $ptr 0
boehmes@52722
  1825
    int
boehmes@52722
  1826
  attribute weight 1
boehmes@52722
  1827
    expr-attr
boehmes@52722
  1828
      int-num 0
boehmes@52722
  1829
fun-decl $read_i8 3 1
boehmes@52722
  1830
    type-con $state 0
boehmes@52722
  1831
    type-con $ptr 0
boehmes@52722
  1832
    int
boehmes@52722
  1833
  attribute weight 1
boehmes@52722
  1834
    expr-attr
boehmes@52722
  1835
      int-num 0
boehmes@52722
  1836
fun-decl $read_u1 3 1
boehmes@52722
  1837
    type-con $state 0
boehmes@52722
  1838
    type-con $ptr 0
boehmes@52722
  1839
    int
boehmes@52722
  1840
  attribute weight 1
boehmes@52722
  1841
    expr-attr
boehmes@52722
  1842
      int-num 0
boehmes@52722
  1843
fun-decl $read_u2 3 1
boehmes@52722
  1844
    type-con $state 0
boehmes@52722
  1845
    type-con $ptr 0
boehmes@52722
  1846
    int
boehmes@52722
  1847
  attribute weight 1
boehmes@52722
  1848
    expr-attr
boehmes@52722
  1849
      int-num 0
boehmes@52722
  1850
fun-decl $read_u4 3 1
boehmes@52722
  1851
    type-con $state 0
boehmes@52722
  1852
    type-con $ptr 0
boehmes@52722
  1853
    int
boehmes@52722
  1854
  attribute weight 1
boehmes@52722
  1855
    expr-attr
boehmes@52722
  1856
      int-num 0
boehmes@52722
  1857
fun-decl $read_u8 3 1
boehmes@52722
  1858
    type-con $state 0
boehmes@52722
  1859
    type-con $ptr 0
boehmes@52722
  1860
    int
boehmes@52722
  1861
  attribute weight 1
boehmes@52722
  1862
    expr-attr
boehmes@52722
  1863
      int-num 0
boehmes@52722
  1864
fun-decl $ptr_to_u8 2 0
boehmes@52722
  1865
    type-con $ptr 0
boehmes@52722
  1866
    int
boehmes@52722
  1867
fun-decl $ptr_to_i8 2 0
boehmes@52722
  1868
    type-con $ptr 0
boehmes@52722
  1869
    int
boehmes@52722
  1870
fun-decl $ptr_to_u4 2 0
boehmes@52722
  1871
    type-con $ptr 0
boehmes@52722
  1872
    int
boehmes@52722
  1873
fun-decl $ptr_to_i4 2 0
boehmes@52722
  1874
    type-con $ptr 0
boehmes@52722
  1875
    int
boehmes@52722
  1876
fun-decl $u8_to_ptr 2 1
boehmes@52722
  1877
    int
boehmes@52722
  1878
    type-con $ptr 0
boehmes@52722
  1879
  attribute inline 1
boehmes@52722
  1880
    expr-attr
boehmes@52722
  1881
      true
boehmes@52722
  1882
fun-decl $i8_to_ptr 2 1
boehmes@52722
  1883
    int
boehmes@52722
  1884
    type-con $ptr 0
boehmes@52722
  1885
  attribute inline 1
boehmes@52722
  1886
    expr-attr
boehmes@52722
  1887
      true
boehmes@52722
  1888
fun-decl $u4_to_ptr 2 1
boehmes@52722
  1889
    int
boehmes@52722
  1890
    type-con $ptr 0
boehmes@52722
  1891
  attribute inline 1
boehmes@52722
  1892
    expr-attr
boehmes@52722
  1893
      true
boehmes@52722
  1894
fun-decl $i4_to_ptr 2 1
boehmes@52722
  1895
    int
boehmes@52722
  1896
    type-con $ptr 0
boehmes@52722
  1897
  attribute inline 1
boehmes@52722
  1898
    expr-attr
boehmes@52722
  1899
      true
boehmes@52722
  1900
fun-decl $byte_ptr_subtraction 3 1
boehmes@52722
  1901
    type-con $ptr 0
boehmes@52722
  1902
    type-con $ptr 0
boehmes@52722
  1903
    int
boehmes@52722
  1904
  attribute weight 1
boehmes@52722
  1905
    expr-attr
boehmes@52722
  1906
      int-num 0
boehmes@52722
  1907
fun-decl $_pow2 2 0
boehmes@52722
  1908
    int
boehmes@52722
  1909
    int
boehmes@52722
  1910
fun-decl $_or 4 0
boehmes@52722
  1911
    type-con $ctype 0
boehmes@52722
  1912
    int
boehmes@52722
  1913
    int
boehmes@52722
  1914
    int
boehmes@52722
  1915
fun-decl $_xor 4 0
boehmes@52722
  1916
    type-con $ctype 0
boehmes@52722
  1917
    int
boehmes@52722
  1918
    int
boehmes@52722
  1919
    int
boehmes@52722
  1920
fun-decl $_and 4 0
boehmes@52722
  1921
    type-con $ctype 0
boehmes@52722
  1922
    int
boehmes@52722
  1923
    int
boehmes@52722
  1924
    int
boehmes@52722
  1925
fun-decl $_not 3 0
boehmes@52722
  1926
    type-con $ctype 0
boehmes@52722
  1927
    int
boehmes@52722
  1928
    int
boehmes@52722
  1929
fun-decl $unchk_add 4 1
boehmes@52722
  1930
    type-con $ctype 0
boehmes@52722
  1931
    int
boehmes@52722
  1932
    int
boehmes@52722
  1933
    int
boehmes@52722
  1934
  attribute weight 1
boehmes@52722
  1935
    expr-attr
boehmes@52722
  1936
      int-num 0
boehmes@52722
  1937
fun-decl $unchk_sub 4 1
boehmes@52722
  1938
    type-con $ctype 0
boehmes@52722
  1939
    int
boehmes@52722
  1940
    int
boehmes@52722
  1941
    int
boehmes@52722
  1942
  attribute weight 1
boehmes@52722
  1943
    expr-attr
boehmes@52722
  1944
      int-num 0
boehmes@52722
  1945
fun-decl $unchk_mul 4 1
boehmes@52722
  1946
    type-con $ctype 0
boehmes@52722
  1947
    int
boehmes@52722
  1948
    int
boehmes@52722
  1949
    int
boehmes@52722
  1950
  attribute weight 1
boehmes@52722
  1951
    expr-attr
boehmes@52722
  1952
      int-num 0
boehmes@52722
  1953
fun-decl $unchk_div 4 1
boehmes@52722
  1954
    type-con $ctype 0
boehmes@52722
  1955
    int
boehmes@52722
  1956
    int
boehmes@52722
  1957
    int
boehmes@52722
  1958
  attribute weight 1
boehmes@52722
  1959
    expr-attr
boehmes@52722
  1960
      int-num 0
boehmes@52722
  1961
fun-decl $unchk_mod 4 1
boehmes@52722
  1962
    type-con $ctype 0
boehmes@52722
  1963
    int
boehmes@52722
  1964
    int
boehmes@52722
  1965
    int
boehmes@52722
  1966
  attribute weight 1
boehmes@52722
  1967
    expr-attr
boehmes@52722
  1968
      int-num 0
boehmes@52722
  1969
fun-decl $_shl 4 1
boehmes@52722
  1970
    type-con $ctype 0
boehmes@52722
  1971
    int
boehmes@52722
  1972
    int
boehmes@52722
  1973
    int
boehmes@52722
  1974
  attribute weight 1
boehmes@52722
  1975
    expr-attr
boehmes@52722
  1976
      int-num 0
boehmes@52722
  1977
fun-decl $_shr 3 1
boehmes@52722
  1978
    int
boehmes@52722
  1979
    int
boehmes@52722
  1980
    int
boehmes@52722
  1981
  attribute weight 1
boehmes@52722
  1982
    expr-attr
boehmes@52722
  1983
      int-num 0
boehmes@52722
  1984
fun-decl $bv_extract_signed 5 0
boehmes@52722
  1985
    int
boehmes@52722
  1986
    int
boehmes@52722
  1987
    int
boehmes@52722
  1988
    int
boehmes@52722
  1989
    int
boehmes@52722
  1990
fun-decl $bv_extract_unsigned 5 0
boehmes@52722
  1991
    int
boehmes@52722
  1992
    int
boehmes@52722
  1993
    int
boehmes@52722
  1994
    int
boehmes@52722
  1995
    int
boehmes@52722
  1996
fun-decl $bv_update 6 0
boehmes@52722
  1997
    int
boehmes@52722
  1998
    int
boehmes@52722
  1999
    int
boehmes@52722
  2000
    int
boehmes@52722
  2001
    int
boehmes@52722
  2002
    int
boehmes@52722
  2003
fun-decl $unchecked 3 0
boehmes@52722
  2004
    type-con $ctype 0
boehmes@52722
  2005
    int
boehmes@52722
  2006
    int
boehmes@52722
  2007
fun-decl $in_range_t 3 0
boehmes@52722
  2008
    type-con $ctype 0
boehmes@52722
  2009
    int
boehmes@52722
  2010
    bool
boehmes@52722
  2011
fun-decl $_mul 3 1
boehmes@52722
  2012
    int
boehmes@52722
  2013
    int
boehmes@52722
  2014
    int
boehmes@52722
  2015
  attribute weight 1
boehmes@52722
  2016
    expr-attr
boehmes@52722
  2017
      int-num 0
boehmes@52722
  2018
fun-decl $get_string_literal 3 0
boehmes@52722
  2019
    int
boehmes@52722
  2020
    int
boehmes@52722
  2021
    type-con $ptr 0
boehmes@52722
  2022
fun-decl $get_fnptr 3 0
boehmes@52722
  2023
    int
boehmes@52722
  2024
    type-con $ctype 0
boehmes@52722
  2025
    type-con $ptr 0
boehmes@52722
  2026
fun-decl $get_fnptr_ref 2 0
boehmes@52722
  2027
    int
boehmes@52722
  2028
    int
boehmes@52722
  2029
fun-decl $get_fnptr_inv 2 0
boehmes@52722
  2030
    int
boehmes@52722
  2031
    int
boehmes@52722
  2032
fun-decl $is_fnptr_type 2 0
boehmes@52722
  2033
    type-con $ctype 0
boehmes@52722
  2034
    bool
boehmes@52722
  2035
fun-decl $is_math_type 2 0
boehmes@52722
  2036
    type-con $ctype 0
boehmes@52722
  2037
    bool
boehmes@52722
  2038
fun-decl $claims_obj 3 0
boehmes@52722
  2039
    type-con $ptr 0
boehmes@52722
  2040
    type-con $ptr 0
boehmes@52722
  2041
    bool
boehmes@52722
  2042
fun-decl $valid_claim 3 0
boehmes@52722
  2043
    type-con $state 0
boehmes@52722
  2044
    type-con $ptr 0
boehmes@52722
  2045
    bool
boehmes@52722
  2046
fun-decl $claim_initial_assumptions 4 1
boehmes@52722
  2047
    type-con $state 0
boehmes@52722
  2048
    type-con $ptr 0
boehmes@52722
  2049
    type-con $token 0
boehmes@52722
  2050
    bool
boehmes@52722
  2051
  attribute inline 1
boehmes@52722
  2052
    expr-attr
boehmes@52722
  2053
      true
boehmes@52722
  2054
fun-decl $claim_transitivity_assumptions 5 1
boehmes@52722
  2055
    type-con $state 0
boehmes@52722
  2056
    type-con $state 0
boehmes@52722
  2057
    type-con $ptr 0
boehmes@52722
  2058
    type-con $token 0
boehmes@52722
  2059
    bool
boehmes@52722
  2060
  attribute inline 1
boehmes@52722
  2061
    expr-attr
boehmes@52722
  2062
      true
boehmes@52722
  2063
fun-decl $valid_claim_impl 3 1
boehmes@52722
  2064
    type-con $state 0
boehmes@52722
  2065
    type-con $state 0
boehmes@52722
  2066
    bool
boehmes@52722
  2067
  attribute inline 1
boehmes@52722
  2068
    expr-attr
boehmes@52722
  2069
      true
boehmes@52722
  2070
fun-decl $claims_claim 3 0
boehmes@52722
  2071
    type-con $ptr 0
boehmes@52722
  2072
    type-con $ptr 0
boehmes@52722
  2073
    bool
boehmes@52722
  2074
fun-decl $not_shared 3 1
boehmes@52722
  2075
    type-con $state 0
boehmes@52722
  2076
    type-con $ptr 0
boehmes@52722
  2077
    bool
boehmes@52722
  2078
  attribute weight 1
boehmes@52722
  2079
    expr-attr
boehmes@52722
  2080
      int-num 0
boehmes@52722
  2081
fun-decl $claimed_closed 3 1
boehmes@52722
  2082
    type-con $state 0
boehmes@52722
  2083
    type-con $ptr 0
boehmes@52722
  2084
    bool
boehmes@52722
  2085
  attribute weight 1
boehmes@52722
  2086
    expr-attr
boehmes@52722
  2087
      int-num 0
boehmes@52722
  2088
fun-decl $no_claim 1 1
boehmes@52722
  2089
    type-con $ptr 0
boehmes@52722
  2090
  attribute unique 0
boehmes@52722
  2091
fun-decl $ref_cnt 3 1
boehmes@52722
  2092
    type-con $state 0
boehmes@52722
  2093
    type-con $ptr 0
boehmes@52722
  2094
    int
boehmes@52722
  2095
  attribute weight 1
boehmes@52722
  2096
    expr-attr
boehmes@52722
  2097
      int-num 0
boehmes@52722
  2098
fun-decl $is_claimable 2 0
boehmes@52722
  2099
    type-con $ctype 0
boehmes@52722
  2100
    bool
boehmes@52722
  2101
fun-decl $is_thread_local_storage 2 0
boehmes@52722
  2102
    type-con $ctype 0
boehmes@52722
  2103
    bool
boehmes@52722
  2104
fun-decl $frame_level 2 0
boehmes@52722
  2105
    type-con $pure_function 0
boehmes@52722
  2106
    int
boehmes@52722
  2107
fun-decl $current_frame_level 1 0
boehmes@52722
  2108
    int
boehmes@52722
  2109
fun-decl $can_use_all_frame_axioms 2 1
boehmes@52722
  2110
    type-con $state 0
boehmes@52722
  2111
    bool
boehmes@52722
  2112
  attribute inline 1
boehmes@52722
  2113
    expr-attr
boehmes@52722
  2114
      true
boehmes@52722
  2115
fun-decl $can_use_frame_axiom_of 2 1
boehmes@52722
  2116
    type-con $pure_function 0
boehmes@52722
  2117
    bool
boehmes@52722
  2118
  attribute inline 1
boehmes@52722
  2119
    expr-attr
boehmes@52722
  2120
      true
boehmes@52722
  2121
fun-decl $reads_check_pre 2 0
boehmes@52722
  2122
    type-con $state 0
boehmes@52722
  2123
    bool
boehmes@52722
  2124
fun-decl $reads_check_post 2 0
boehmes@52722
  2125
    type-con $state 0
boehmes@52722
  2126
    bool
boehmes@52722
  2127
fun-decl $start_here 1 0
boehmes@52722
  2128
    bool
boehmes@52722
  2129
fun-decl $ptrset_to_int 2 0
boehmes@52722
  2130
    type-con $ptrset 0
boehmes@52722
  2131
    int
boehmes@52722
  2132
fun-decl $int_to_ptrset 2 0
boehmes@52722
  2133
    int
boehmes@52722
  2134
    type-con $ptrset 0
boehmes@52722
  2135
fun-decl $version_to_int 2 0
boehmes@52722
  2136
    type-con $version 0
boehmes@52722
  2137
    int
boehmes@52722
  2138
fun-decl $int_to_version 2 0
boehmes@52722
  2139
    int
boehmes@52722
  2140
    type-con $version 0
boehmes@52722
  2141
fun-decl $vol_version_to_int 2 0
boehmes@52722
  2142
    type-con $vol_version 0
boehmes@52722
  2143
    int
boehmes@52722
  2144
fun-decl $int_to_vol_version 2 0
boehmes@52722
  2145
    int
boehmes@52722
  2146
    type-con $vol_version 0
boehmes@52722
  2147
fun-decl $ptr_to_int 2 0
boehmes@52722
  2148
    type-con $ptr 0
boehmes@52722
  2149
    int
boehmes@52722
  2150
fun-decl $int_to_ptr 2 0
boehmes@52722
  2151
    int
boehmes@52722
  2152
    type-con $ptr 0
boehmes@52722
  2153
fun-decl $precise_test 2 0
boehmes@52722
  2154
    type-con $ptr 0
boehmes@52722
  2155
    bool
boehmes@52722
  2156
fun-decl $updated_only_values 4 0
boehmes@52722
  2157
    type-con $state 0
boehmes@52722
  2158
    type-con $state 0
boehmes@52722
  2159
    type-con $ptrset 0
boehmes@52722
  2160
    bool
boehmes@52722
  2161
fun-decl $updated_only_domains 4 0
boehmes@52722
  2162
    type-con $state 0
boehmes@52722
  2163
    type-con $state 0
boehmes@52722
  2164
    type-con $ptrset 0
boehmes@52722
  2165
    bool
boehmes@52722
  2166
fun-decl $domain_updated_at 5 0
boehmes@52722
  2167
    type-con $state 0
boehmes@52722
  2168
    type-con $state 0
boehmes@52722
  2169
    type-con $ptr 0
boehmes@52722
  2170
    type-con $ptrset 0
boehmes@52722
  2171
    bool
boehmes@52722
  2172
fun-decl l#public 1 1
boehmes@52722
  2173
    type-con $label 0
boehmes@52722
  2174
  attribute unique 0
boehmes@52722
  2175
fun-decl #tok$1^16.24 1 1
boehmes@52722
  2176
    type-con $token 0
boehmes@52722
  2177
  attribute unique 0
boehmes@52722
  2178
fun-decl #tok$1^24.47 1 1
boehmes@52722
  2179
    type-con $token 0
boehmes@52722
  2180
  attribute unique 0
boehmes@52722
  2181
fun-decl #tok$1^23.7 1 1
boehmes@52722
  2182
    type-con $token 0
boehmes@52722
  2183
  attribute unique 0
boehmes@52722
  2184
fun-decl #tok$1^16.3 1 1
boehmes@52722
  2185
    type-con $token 0
boehmes@52722
  2186
  attribute unique 0
boehmes@52722
  2187
fun-decl #loc.p 1 1