src/HOL/Boogie/Examples/VCC_Max.b2i
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 33419 8ae45e87b992
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
boehmes@33419
     1
type-decl $ctype 0 0
boehmes@33419
     2
type-decl $ptr 0 0
boehmes@33419
     3
type-decl $field 0 0
boehmes@33419
     4
type-decl $kind 0 0
boehmes@33419
     5
type-decl $type_state 0 0
boehmes@33419
     6
type-decl $status 0 0
boehmes@33419
     7
type-decl $primitive 0 0
boehmes@33419
     8
type-decl $struct 0 0
boehmes@33419
     9
type-decl $token 0 0
boehmes@33419
    10
type-decl $state 0 0
boehmes@33419
    11
type-decl $pure_function 0 0
boehmes@33419
    12
type-decl $label 0 0
boehmes@33419
    13
type-decl $memory_t 0 0
boehmes@33419
    14
type-decl $typemap_t 0 0
boehmes@33419
    15
type-decl $statusmap_t 0 0
boehmes@33419
    16
type-decl $record 0 0
boehmes@33419
    17
type-decl $version 0 0
boehmes@33419
    18
type-decl $vol_version 0 0
boehmes@33419
    19
type-decl $ptrset 0 0
boehmes@33419
    20
fun-decl $kind_of 2 0
boehmes@33419
    21
    type-con $ctype 0
boehmes@33419
    22
    type-con $kind 0
boehmes@33419
    23
fun-decl $kind_composite 1 1
boehmes@33419
    24
    type-con $kind 0
boehmes@33419
    25
  attribute unique 0
boehmes@33419
    26
fun-decl $kind_primitive 1 1
boehmes@33419
    27
    type-con $kind 0
boehmes@33419
    28
  attribute unique 0
boehmes@33419
    29
fun-decl $kind_array 1 1
boehmes@33419
    30
    type-con $kind 0
boehmes@33419
    31
  attribute unique 0
boehmes@33419
    32
fun-decl $kind_thread 1 1
boehmes@33419
    33
    type-con $kind 0
boehmes@33419
    34
  attribute unique 0
boehmes@33419
    35
fun-decl $sizeof 2 0
boehmes@33419
    36
    type-con $ctype 0
boehmes@33419
    37
    int
boehmes@33419
    38
fun-decl ^^i1 1 1
boehmes@33419
    39
    type-con $ctype 0
boehmes@33419
    40
  attribute unique 0
boehmes@33419
    41
fun-decl ^^i2 1 1
boehmes@33419
    42
    type-con $ctype 0
boehmes@33419
    43
  attribute unique 0
boehmes@33419
    44
fun-decl ^^i4 1 1
boehmes@33419
    45
    type-con $ctype 0
boehmes@33419
    46
  attribute unique 0
boehmes@33419
    47
fun-decl ^^i8 1 1
boehmes@33419
    48
    type-con $ctype 0
boehmes@33419
    49
  attribute unique 0
boehmes@33419
    50
fun-decl ^^u1 1 1
boehmes@33419
    51
    type-con $ctype 0
boehmes@33419
    52
  attribute unique 0
boehmes@33419
    53
fun-decl ^^u2 1 1
boehmes@33419
    54
    type-con $ctype 0
boehmes@33419
    55
  attribute unique 0
boehmes@33419
    56
fun-decl ^^u4 1 1
boehmes@33419
    57
    type-con $ctype 0
boehmes@33419
    58
  attribute unique 0
boehmes@33419
    59
fun-decl ^^u8 1 1
boehmes@33419
    60
    type-con $ctype 0
boehmes@33419
    61
  attribute unique 0
boehmes@33419
    62
fun-decl ^^void 1 1
boehmes@33419
    63
    type-con $ctype 0
boehmes@33419
    64
  attribute unique 0
boehmes@33419
    65
fun-decl ^^bool 1 1
boehmes@33419
    66
    type-con $ctype 0
boehmes@33419
    67
  attribute unique 0
boehmes@33419
    68
fun-decl ^^f4 1 1
boehmes@33419
    69
    type-con $ctype 0
boehmes@33419
    70
  attribute unique 0
boehmes@33419
    71
fun-decl ^^f8 1 1
boehmes@33419
    72
    type-con $ctype 0
boehmes@33419
    73
  attribute unique 0
boehmes@33419
    74
fun-decl ^^claim 1 1
boehmes@33419
    75
    type-con $ctype 0
boehmes@33419
    76
  attribute unique 0
boehmes@33419
    77
fun-decl ^^root_emb 1 1
boehmes@33419
    78
    type-con $ctype 0
boehmes@33419
    79
  attribute unique 0
boehmes@33419
    80
fun-decl ^^mathint 1 1
boehmes@33419
    81
    type-con $ctype 0
boehmes@33419
    82
  attribute unique 0
boehmes@33419
    83
fun-decl ^$#thread_id_t 1 1
boehmes@33419
    84
    type-con $ctype 0
boehmes@33419
    85
  attribute unique 0
boehmes@33419
    86
fun-decl ^$#ptrset 1 1
boehmes@33419
    87
    type-con $ctype 0
boehmes@33419
    88
  attribute unique 0
boehmes@33419
    89
fun-decl ^$#state_t 1 1
boehmes@33419
    90
    type-con $ctype 0
boehmes@33419
    91
  attribute unique 0
boehmes@33419
    92
fun-decl ^$#struct 1 1
boehmes@33419
    93
    type-con $ctype 0
boehmes@33419
    94
  attribute unique 0
boehmes@33419
    95
fun-decl $ptr_to 2 0
boehmes@33419
    96
    type-con $ctype 0
boehmes@33419
    97
    type-con $ctype 0
boehmes@33419
    98
fun-decl $unptr_to 2 0
boehmes@33419
    99
    type-con $ctype 0
boehmes@33419
   100
    type-con $ctype 0
boehmes@33419
   101
fun-decl $ptr_level 2 0
boehmes@33419
   102
    type-con $ctype 0
boehmes@33419
   103
    int
boehmes@33419
   104
fun-decl $map_t 3 0
boehmes@33419
   105
    type-con $ctype 0
boehmes@33419
   106
    type-con $ctype 0
boehmes@33419
   107
    type-con $ctype 0
boehmes@33419
   108
fun-decl $map_domain 2 0
boehmes@33419
   109
    type-con $ctype 0
boehmes@33419
   110
    type-con $ctype 0
boehmes@33419
   111
fun-decl $map_range 2 0
boehmes@33419
   112
    type-con $ctype 0
boehmes@33419
   113
    type-con $ctype 0
boehmes@33419
   114
fun-decl $is_primitive 2 1
boehmes@33419
   115
    type-con $ctype 0
boehmes@33419
   116
    bool
boehmes@33419
   117
  attribute weight 1
boehmes@33419
   118
    expr-attr
boehmes@33419
   119
      int-num 0
boehmes@33419
   120
fun-decl $is_primitive_ch 2 1
boehmes@33419
   121
    type-con $ctype 0
boehmes@33419
   122
    bool
boehmes@33419
   123
  attribute inline 1
boehmes@33419
   124
    expr-attr
boehmes@33419
   125
      true
boehmes@33419
   126
fun-decl $is_composite 2 1
boehmes@33419
   127
    type-con $ctype 0
boehmes@33419
   128
    bool
boehmes@33419
   129
  attribute weight 1
boehmes@33419
   130
    expr-attr
boehmes@33419
   131
      int-num 0
boehmes@33419
   132
fun-decl $is_composite_ch 2 1
boehmes@33419
   133
    type-con $ctype 0
boehmes@33419
   134
    bool
boehmes@33419
   135
  attribute inline 1
boehmes@33419
   136
    expr-attr
boehmes@33419
   137
      true
boehmes@33419
   138
fun-decl $is_arraytype 2 1
boehmes@33419
   139
    type-con $ctype 0
boehmes@33419
   140
    bool
boehmes@33419
   141
  attribute weight 1
boehmes@33419
   142
    expr-attr
boehmes@33419
   143
      int-num 0
boehmes@33419
   144
fun-decl $is_arraytype_ch 2 1
boehmes@33419
   145
    type-con $ctype 0
boehmes@33419
   146
    bool
boehmes@33419
   147
  attribute inline 1
boehmes@33419
   148
    expr-attr
boehmes@33419
   149
      true
boehmes@33419
   150
fun-decl $is_threadtype 2 1
boehmes@33419
   151
    type-con $ctype 0
boehmes@33419
   152
    bool
boehmes@33419
   153
  attribute weight 1
boehmes@33419
   154
    expr-attr
boehmes@33419
   155
      int-num 0
boehmes@33419
   156
fun-decl $is_thread 2 1
boehmes@33419
   157
    type-con $ptr 0
boehmes@33419
   158
    bool
boehmes@33419
   159
  attribute inline 1
boehmes@33419
   160
    expr-attr
boehmes@33419
   161
      true
boehmes@33419
   162
fun-decl $is_ptr_to_composite 2 1
boehmes@33419
   163
    type-con $ptr 0
boehmes@33419
   164
    bool
boehmes@33419
   165
  attribute inline 1
boehmes@33419
   166
    expr-attr
boehmes@33419
   167
      true
boehmes@33419
   168
fun-decl $field_offset 2 0
boehmes@33419
   169
    type-con $field 0
boehmes@33419
   170
    int
boehmes@33419
   171
fun-decl $field_parent_type 2 0
boehmes@33419
   172
    type-con $field 0
boehmes@33419
   173
    type-con $ctype 0
boehmes@33419
   174
fun-decl $is_non_primitive 2 0
boehmes@33419
   175
    type-con $ctype 0
boehmes@33419
   176
    bool
boehmes@33419
   177
fun-decl $is_non_primitive_ch 2 1
boehmes@33419
   178
    type-con $ctype 0
boehmes@33419
   179
    bool
boehmes@33419
   180
  attribute inline 1
boehmes@33419
   181
    expr-attr
boehmes@33419
   182
      true
boehmes@33419
   183
fun-decl $is_non_primitive_ptr 2 1
boehmes@33419
   184
    type-con $ptr 0
boehmes@33419
   185
    bool
boehmes@33419
   186
  attribute inline 1
boehmes@33419
   187
    expr-attr
boehmes@33419
   188
      true
boehmes@33419
   189
fun-decl $me_ref 1 0
boehmes@33419
   190
    int
boehmes@33419
   191
fun-decl $me 1 0
boehmes@33419
   192
    type-con $ptr 0
boehmes@33419
   193
fun-decl $current_state 2 1
boehmes@33419
   194
    type-con $state 0
boehmes@33419
   195
    type-con $state 0
boehmes@33419
   196
  attribute inline 1
boehmes@33419
   197
    expr-attr
boehmes@33419
   198
      true
boehmes@33419
   199
fun-decl $select.mem 3 0
boehmes@33419
   200
    type-con $memory_t 0
boehmes@33419
   201
    type-con $ptr 0
boehmes@33419
   202
    int
boehmes@33419
   203
fun-decl $store.mem 4 0
boehmes@33419
   204
    type-con $memory_t 0
boehmes@33419
   205
    type-con $ptr 0
boehmes@33419
   206
    int
boehmes@33419
   207
    type-con $memory_t 0
boehmes@33419
   208
fun-decl $select.tm 3 0
boehmes@33419
   209
    type-con $typemap_t 0
boehmes@33419
   210
    type-con $ptr 0
boehmes@33419
   211
    type-con $type_state 0
boehmes@33419
   212
fun-decl $store.tm 4 0
boehmes@33419
   213
    type-con $typemap_t 0
boehmes@33419
   214
    type-con $ptr 0
boehmes@33419
   215
    type-con $type_state 0
boehmes@33419
   216
    type-con $typemap_t 0
boehmes@33419
   217
fun-decl $select.sm 3 0
boehmes@33419
   218
    type-con $statusmap_t 0
boehmes@33419
   219
    type-con $ptr 0
boehmes@33419
   220
    type-con $status 0
boehmes@33419
   221
fun-decl $store.sm 4 0
boehmes@33419
   222
    type-con $statusmap_t 0
boehmes@33419
   223
    type-con $ptr 0
boehmes@33419
   224
    type-con $status 0
boehmes@33419
   225
    type-con $statusmap_t 0
boehmes@33419
   226
fun-decl $memory 2 0
boehmes@33419
   227
    type-con $state 0
boehmes@33419
   228
    type-con $memory_t 0
boehmes@33419
   229
fun-decl $typemap 2 0
boehmes@33419
   230
    type-con $state 0
boehmes@33419
   231
    type-con $typemap_t 0
boehmes@33419
   232
fun-decl $statusmap 2 0
boehmes@33419
   233
    type-con $state 0
boehmes@33419
   234
    type-con $statusmap_t 0
boehmes@33419
   235
fun-decl $mem 3 1
boehmes@33419
   236
    type-con $state 0
boehmes@33419
   237
    type-con $ptr 0
boehmes@33419
   238
    int
boehmes@33419
   239
  attribute inline 1
boehmes@33419
   240
    expr-attr
boehmes@33419
   241
      true
boehmes@33419
   242
fun-decl $read_any 3 1
boehmes@33419
   243
    type-con $state 0
boehmes@33419
   244
    type-con $ptr 0
boehmes@33419
   245
    int
boehmes@33419
   246
  attribute inline 1
boehmes@33419
   247
    expr-attr
boehmes@33419
   248
      true
boehmes@33419
   249
fun-decl $mem_eq 4 1
boehmes@33419
   250
    type-con $state 0
boehmes@33419
   251
    type-con $state 0
boehmes@33419
   252
    type-con $ptr 0
boehmes@33419
   253
    bool
boehmes@33419
   254
  attribute inline 1
boehmes@33419
   255
    expr-attr
boehmes@33419
   256
      true
boehmes@33419
   257
fun-decl $st_eq 4 1
boehmes@33419
   258
    type-con $state 0
boehmes@33419
   259
    type-con $state 0
boehmes@33419
   260
    type-con $ptr 0
boehmes@33419
   261
    bool
boehmes@33419
   262
  attribute inline 1
boehmes@33419
   263
    expr-attr
boehmes@33419
   264
      true
boehmes@33419
   265
fun-decl $ts_eq 4 1
boehmes@33419
   266
    type-con $state 0
boehmes@33419
   267
    type-con $state 0
boehmes@33419
   268
    type-con $ptr 0
boehmes@33419
   269
    bool
boehmes@33419
   270
  attribute inline 1
boehmes@33419
   271
    expr-attr
boehmes@33419
   272
      true
boehmes@33419
   273
fun-decl $extent_hint 3 0
boehmes@33419
   274
    type-con $ptr 0
boehmes@33419
   275
    type-con $ptr 0
boehmes@33419
   276
    bool
boehmes@33419
   277
fun-decl $nesting_level 2 0
boehmes@33419
   278
    type-con $ctype 0
boehmes@33419
   279
    int
boehmes@33419
   280
fun-decl $is_nested 3 0
boehmes@33419
   281
    type-con $ctype 0
boehmes@33419
   282
    type-con $ctype 0
boehmes@33419
   283
    bool
boehmes@33419
   284
fun-decl $nesting_min 3 0
boehmes@33419
   285
    type-con $ctype 0
boehmes@33419
   286
    type-con $ctype 0
boehmes@33419
   287
    int
boehmes@33419
   288
fun-decl $nesting_max 3 0
boehmes@33419
   289
    type-con $ctype 0
boehmes@33419
   290
    type-con $ctype 0
boehmes@33419
   291
    int
boehmes@33419
   292
fun-decl $is_nested_range 5 0
boehmes@33419
   293
    type-con $ctype 0
boehmes@33419
   294
    type-con $ctype 0
boehmes@33419
   295
    int
boehmes@33419
   296
    int
boehmes@33419
   297
    bool
boehmes@33419
   298
fun-decl $typ 2 0
boehmes@33419
   299
    type-con $ptr 0
boehmes@33419
   300
    type-con $ctype 0
boehmes@33419
   301
fun-decl $ref 2 0
boehmes@33419
   302
    type-con $ptr 0
boehmes@33419
   303
    int
boehmes@33419
   304
fun-decl $ptr 3 0
boehmes@33419
   305
    type-con $ctype 0
boehmes@33419
   306
    int
boehmes@33419
   307
    type-con $ptr 0
boehmes@33419
   308
fun-decl $ghost_ref 3 0
boehmes@33419
   309
    type-con $ptr 0
boehmes@33419
   310
    type-con $field 0
boehmes@33419
   311
    int
boehmes@33419
   312
fun-decl $ghost_emb 2 0
boehmes@33419
   313
    int
boehmes@33419
   314
    type-con $ptr 0
boehmes@33419
   315
fun-decl $ghost_path 2 0
boehmes@33419
   316
    int
boehmes@33419
   317
    type-con $field 0
boehmes@33419
   318
fun-decl $physical_ref 3 0
boehmes@33419
   319
    type-con $ptr 0
boehmes@33419
   320
    type-con $field 0
boehmes@33419
   321
    int
boehmes@33419
   322
fun-decl $array_path 3 0
boehmes@33419
   323
    type-con $field 0
boehmes@33419
   324
    int
boehmes@33419
   325
    type-con $field 0
boehmes@33419
   326
fun-decl $is_base_field 2 0
boehmes@33419
   327
    type-con $field 0
boehmes@33419
   328
    bool
boehmes@33419
   329
fun-decl $array_path_1 2 0
boehmes@33419
   330
    type-con $field 0
boehmes@33419
   331
    type-con $field 0
boehmes@33419
   332
fun-decl $array_path_2 2 0
boehmes@33419
   333
    type-con $field 0
boehmes@33419
   334
    int
boehmes@33419
   335
fun-decl $null 1 0
boehmes@33419
   336
    type-con $ptr 0
boehmes@33419
   337
fun-decl $is 3 0
boehmes@33419
   338
    type-con $ptr 0
boehmes@33419
   339
    type-con $ctype 0
boehmes@33419
   340
    bool
boehmes@33419
   341
fun-decl $ptr_cast 3 1
boehmes@33419
   342
    type-con $ptr 0
boehmes@33419
   343
    type-con $ctype 0
boehmes@33419
   344
    type-con $ptr 0
boehmes@33419
   345
  attribute inline 1
boehmes@33419
   346
    expr-attr
boehmes@33419
   347
      true
boehmes@33419
   348
fun-decl $read_ptr 4 1
boehmes@33419
   349
    type-con $state 0
boehmes@33419
   350
    type-con $ptr 0
boehmes@33419
   351
    type-con $ctype 0
boehmes@33419
   352
    type-con $ptr 0
boehmes@33419
   353
  attribute inline 1
boehmes@33419
   354
    expr-attr
boehmes@33419
   355
      true
boehmes@33419
   356
fun-decl $dot 3 0
boehmes@33419
   357
    type-con $ptr 0
boehmes@33419
   358
    type-con $field 0
boehmes@33419
   359
    type-con $ptr 0
boehmes@33419
   360
fun-decl $emb 3 1
boehmes@33419
   361
    type-con $state 0
boehmes@33419
   362
    type-con $ptr 0
boehmes@33419
   363
    type-con $ptr 0
boehmes@33419
   364
  attribute inline 1
boehmes@33419
   365
    expr-attr
boehmes@33419
   366
      true
boehmes@33419
   367
fun-decl $path 3 1
boehmes@33419
   368
    type-con $state 0
boehmes@33419
   369
    type-con $ptr 0
boehmes@33419
   370
    type-con $field 0
boehmes@33419
   371
  attribute inline 1
boehmes@33419
   372
    expr-attr
boehmes@33419
   373
      true
boehmes@33419
   374
fun-decl $containing_struct 3 0
boehmes@33419
   375
    type-con $ptr 0
boehmes@33419
   376
    type-con $field 0
boehmes@33419
   377
    type-con $ptr 0
boehmes@33419
   378
fun-decl $containing_struct_ref 3 0
boehmes@33419
   379
    type-con $ptr 0
boehmes@33419
   380
    type-con $field 0
boehmes@33419
   381
    int
boehmes@33419
   382
fun-decl $is_primitive_non_volatile_field 2 0
boehmes@33419
   383
    type-con $field 0
boehmes@33419
   384
    bool
boehmes@33419
   385
fun-decl $is_primitive_volatile_field 2 0
boehmes@33419
   386
    type-con $field 0
boehmes@33419
   387
    bool
boehmes@33419
   388
fun-decl $is_primitive_embedded_array 3 0
boehmes@33419
   389
    type-con $field 0
boehmes@33419
   390
    int
boehmes@33419
   391
    bool
boehmes@33419
   392
fun-decl $is_primitive_embedded_volatile_array 4 0
boehmes@33419
   393
    type-con $field 0
boehmes@33419
   394
    int
boehmes@33419
   395
    type-con $ctype 0
boehmes@33419
   396
    bool
boehmes@33419
   397
fun-decl $static_field_properties 3 1
boehmes@33419
   398
    type-con $field 0
boehmes@33419
   399
    type-con $ctype 0
boehmes@33419
   400
    bool
boehmes@33419
   401
  attribute inline 1
boehmes@33419
   402
    expr-attr
boehmes@33419
   403
      true
boehmes@33419
   404
fun-decl $field_properties 6 1
boehmes@33419
   405
    type-con $state 0
boehmes@33419
   406
    type-con $ptr 0
boehmes@33419
   407
    type-con $field 0
boehmes@33419
   408
    type-con $ctype 0
boehmes@33419
   409
    bool
boehmes@33419
   410
    bool
boehmes@33419
   411
  attribute inline 1
boehmes@33419
   412
    expr-attr
boehmes@33419
   413
      true
boehmes@33419
   414
fun-decl $ts_typed 2 0
boehmes@33419
   415
    type-con $type_state 0
boehmes@33419
   416
    bool
boehmes@33419
   417
fun-decl $ts_emb 2 0
boehmes@33419
   418
    type-con $type_state 0
boehmes@33419
   419
    type-con $ptr 0
boehmes@33419
   420
fun-decl $ts_path 2 0
boehmes@33419
   421
    type-con $type_state 0
boehmes@33419
   422
    type-con $field 0
boehmes@33419
   423
fun-decl $ts_is_array_elt 2 0
boehmes@33419
   424
    type-con $type_state 0
boehmes@33419
   425
    bool
boehmes@33419
   426
fun-decl $ts_is_volatile 2 0
boehmes@33419
   427
    type-con $type_state 0
boehmes@33419
   428
    bool
boehmes@33419
   429
fun-decl $is_object_root 3 1
boehmes@33419
   430
    type-con $state 0
boehmes@33419
   431
    type-con $ptr 0
boehmes@33419
   432
    bool
boehmes@33419
   433
  attribute inline 1
boehmes@33419
   434
    expr-attr
boehmes@33419
   435
      true
boehmes@33419
   436
fun-decl $is_volatile 3 1
boehmes@33419
   437
    type-con $state 0
boehmes@33419
   438
    type-con $ptr 0
boehmes@33419
   439
    bool
boehmes@33419
   440
  attribute inline 1
boehmes@33419
   441
    expr-attr
boehmes@33419
   442
      true
boehmes@33419
   443
fun-decl $is_malloc_root 3 1
boehmes@33419
   444
    type-con $state 0
boehmes@33419
   445
    type-con $ptr 0
boehmes@33419
   446
    bool
boehmes@33419
   447
  attribute inline 1
boehmes@33419
   448
    expr-attr
boehmes@33419
   449
      true
boehmes@33419
   450
fun-decl $current_timestamp 2 0
boehmes@33419
   451
    type-con $state 0
boehmes@33419
   452
    int
boehmes@33419
   453
fun-decl $is_fresh 4 1
boehmes@33419
   454
    type-con $state 0
boehmes@33419
   455
    type-con $state 0
boehmes@33419
   456
    type-con $ptr 0
boehmes@33419
   457
    bool
boehmes@33419
   458
  attribute inline 1
boehmes@33419
   459
    expr-attr
boehmes@33419
   460
      true
boehmes@33419
   461
fun-decl $in_writes_at 3 0
boehmes@33419
   462
    int
boehmes@33419
   463
    type-con $ptr 0
boehmes@33419
   464
    bool
boehmes@33419
   465
fun-decl $writable 4 1
boehmes@33419
   466
    type-con $state 0
boehmes@33419
   467
    int
boehmes@33419
   468
    type-con $ptr 0
boehmes@33419
   469
    bool
boehmes@33419
   470
  attribute inline 1
boehmes@33419
   471
    expr-attr
boehmes@33419
   472
      true
boehmes@33419
   473
fun-decl $top_writable 4 1
boehmes@33419
   474
    type-con $state 0
boehmes@33419
   475
    int
boehmes@33419
   476
    type-con $ptr 0
boehmes@33419
   477
    bool
boehmes@33419
   478
  attribute inline 1
boehmes@33419
   479
    expr-attr
boehmes@33419
   480
      true
boehmes@33419
   481
fun-decl $struct_zero 1 0
boehmes@33419
   482
    type-con $struct 0
boehmes@33419
   483
fun-decl $vs_base 3 1
boehmes@33419
   484
    type-con $struct 0
boehmes@33419
   485
    type-con $ctype 0
boehmes@33419
   486
    type-con $ptr 0
boehmes@33419
   487
  attribute inline 1
boehmes@33419
   488
    expr-attr
boehmes@33419
   489
      true
boehmes@33419
   490
fun-decl $vs_base_ref 2 0
boehmes@33419
   491
    type-con $struct 0
boehmes@33419
   492
    int
boehmes@33419
   493
fun-decl $vs_state 2 0
boehmes@33419
   494
    type-con $struct 0
boehmes@33419
   495
    type-con $state 0
boehmes@33419
   496
fun-decl $vs_ctor 3 0
boehmes@33419
   497
    type-con $state 0
boehmes@33419
   498
    type-con $ptr 0
boehmes@33419
   499
    type-con $struct 0
boehmes@33419
   500
fun-decl $rec_zero 1 0
boehmes@33419
   501
    type-con $record 0
boehmes@33419
   502
fun-decl $rec_update 4 0
boehmes@33419
   503
    type-con $record 0
boehmes@33419
   504
    type-con $field 0
boehmes@33419
   505
    int
boehmes@33419
   506
    type-con $record 0
boehmes@33419
   507
fun-decl $rec_fetch 3 0
boehmes@33419
   508
    type-con $record 0
boehmes@33419
   509
    type-con $field 0
boehmes@33419
   510
    int
boehmes@33419
   511
fun-decl $rec_update_bv 7 0
boehmes@33419
   512
    type-con $record 0
boehmes@33419
   513
    type-con $field 0
boehmes@33419
   514
    int
boehmes@33419
   515
    int
boehmes@33419
   516
    int
boehmes@33419
   517
    int
boehmes@33419
   518
    type-con $record 0
boehmes@33419
   519
fun-decl $is_record_type 2 0
boehmes@33419
   520
    type-con $ctype 0
boehmes@33419
   521
    bool
boehmes@33419
   522
fun-decl $is_record_field 4 0
boehmes@33419
   523
    type-con $ctype 0
boehmes@33419
   524
    type-con $field 0
boehmes@33419
   525
    type-con $ctype 0
boehmes@33419
   526
    bool
boehmes@33419
   527
fun-decl $as_record_record_field 2 0
boehmes@33419
   528
    type-con $field 0
boehmes@33419
   529
    type-con $field 0
boehmes@33419
   530
fun-decl $rec_eq 3 0
boehmes@33419
   531
    type-con $record 0
boehmes@33419
   532
    type-con $record 0
boehmes@33419
   533
    bool
boehmes@33419
   534
fun-decl $rec_base_eq 3 0
boehmes@33419
   535
    int
boehmes@33419
   536
    int
boehmes@33419
   537
    bool
boehmes@33419
   538
fun-decl $int_to_record 2 0
boehmes@33419
   539
    int
boehmes@33419
   540
    type-con $record 0
boehmes@33419
   541
fun-decl $record_to_int 2 0
boehmes@33419
   542
    type-con $record 0
boehmes@33419
   543
    int
boehmes@33419
   544
fun-decl $good_state 2 0
boehmes@33419
   545
    type-con $state 0
boehmes@33419
   546
    bool
boehmes@33419
   547
fun-decl $invok_state 2 0
boehmes@33419
   548
    type-con $state 0
boehmes@33419
   549
    bool
boehmes@33419
   550
fun-decl $has_volatile_owns_set 2 0
boehmes@33419
   551
    type-con $ctype 0
boehmes@33419
   552
    bool
boehmes@33419
   553
fun-decl $owns_set_field 2 0
boehmes@33419
   554
    type-con $ctype 0
boehmes@33419
   555
    type-con $field 0
boehmes@33419
   556
fun-decl $st_owner 2 0
boehmes@33419
   557
    type-con $status 0
boehmes@33419
   558
    type-con $ptr 0
boehmes@33419
   559
fun-decl $st_closed 2 0
boehmes@33419
   560
    type-con $status 0
boehmes@33419
   561
    bool
boehmes@33419
   562
fun-decl $st_timestamp 2 0
boehmes@33419
   563
    type-con $status 0
boehmes@33419
   564
    int
boehmes@33419
   565
fun-decl $st_ref_cnt 2 0
boehmes@33419
   566
    type-con $status 0
boehmes@33419
   567
    int
boehmes@33419
   568
fun-decl $owner 3 0
boehmes@33419
   569
    type-con $state 0
boehmes@33419
   570
    type-con $ptr 0
boehmes@33419
   571
    type-con $ptr 0
boehmes@33419
   572
fun-decl $closed 3 0
boehmes@33419
   573
    type-con $state 0
boehmes@33419
   574
    type-con $ptr 0
boehmes@33419
   575
    bool
boehmes@33419
   576
fun-decl $timestamp 3 0
boehmes@33419
   577
    type-con $state 0
boehmes@33419
   578
    type-con $ptr 0
boehmes@33419
   579
    int
boehmes@33419
   580
fun-decl $position_marker 1 0
boehmes@33419
   581
    bool
boehmes@33419
   582
fun-decl $st 3 1
boehmes@33419
   583
    type-con $state 0
boehmes@33419
   584
    type-con $ptr 0
boehmes@33419
   585
    type-con $status 0
boehmes@33419
   586
  attribute inline 1
boehmes@33419
   587
    expr-attr
boehmes@33419
   588
      true
boehmes@33419
   589
fun-decl $ts 3 1
boehmes@33419
   590
    type-con $state 0
boehmes@33419
   591
    type-con $ptr 0
boehmes@33419
   592
    type-con $type_state 0
boehmes@33419
   593
  attribute inline 1
boehmes@33419
   594
    expr-attr
boehmes@33419
   595
      true
boehmes@33419
   596
fun-decl $owns 3 1
boehmes@33419
   597
    type-con $state 0
boehmes@33419
   598
    type-con $ptr 0
boehmes@33419
   599
    type-con $ptrset 0
boehmes@33419
   600
  attribute weight 1
boehmes@33419
   601
    expr-attr
boehmes@33419
   602
      int-num 0
boehmes@33419
   603
fun-decl $nested 3 1
boehmes@33419
   604
    type-con $state 0
boehmes@33419
   605
    type-con $ptr 0
boehmes@33419
   606
    bool
boehmes@33419
   607
  attribute inline 1
boehmes@33419
   608
    expr-attr
boehmes@33419
   609
      true
boehmes@33419
   610
fun-decl $nested_in 4 1
boehmes@33419
   611
    type-con $state 0
boehmes@33419
   612
    type-con $ptr 0
boehmes@33419
   613
    type-con $ptr 0
boehmes@33419
   614
    bool
boehmes@33419
   615
  attribute inline 1
boehmes@33419
   616
    expr-attr
boehmes@33419
   617
      true
boehmes@33419
   618
fun-decl $wrapped 4 1
boehmes@33419
   619
    type-con $state 0
boehmes@33419
   620
    type-con $ptr 0
boehmes@33419
   621
    type-con $ctype 0
boehmes@33419
   622
    bool
boehmes@33419
   623
  attribute inline 1
boehmes@33419
   624
    expr-attr
boehmes@33419
   625
      true
boehmes@33419
   626
fun-decl $irrelevant 3 1
boehmes@33419
   627
    type-con $state 0
boehmes@33419
   628
    type-con $ptr 0
boehmes@33419
   629
    bool
boehmes@33419
   630
  attribute inline 1
boehmes@33419
   631
    expr-attr
boehmes@33419
   632
      true
boehmes@33419
   633
fun-decl $mutable 3 1
boehmes@33419
   634
    type-con $state 0
boehmes@33419
   635
    type-con $ptr 0
boehmes@33419
   636
    bool
boehmes@33419
   637
  attribute weight 1
boehmes@33419
   638
    expr-attr
boehmes@33419
   639
      int-num 0
boehmes@33419
   640
fun-decl $thread_owned 3 1
boehmes@33419
   641
    type-con $state 0
boehmes@33419
   642
    type-con $ptr 0
boehmes@33419
   643
    bool
boehmes@33419
   644
  attribute inline 1
boehmes@33419
   645
    expr-attr
boehmes@33419
   646
      true
boehmes@33419
   647
fun-decl $thread_owned_or_even_mutable 3 1
boehmes@33419
   648
    type-con $state 0
boehmes@33419
   649
    type-con $ptr 0
boehmes@33419
   650
    bool
boehmes@33419
   651
  attribute inline 1
boehmes@33419
   652
    expr-attr
boehmes@33419
   653
      true
boehmes@33419
   654
fun-decl $typed 3 0
boehmes@33419
   655
    type-con $state 0
boehmes@33419
   656
    type-con $ptr 0
boehmes@33419
   657
    bool
boehmes@33419
   658
fun-decl $typed2 4 1
boehmes@33419
   659
    type-con $state 0
boehmes@33419
   660
    type-con $ptr 0
boehmes@33419
   661
    type-con $ctype 0
boehmes@33419
   662
    bool
boehmes@33419
   663
  attribute inline 1
boehmes@33419
   664
    expr-attr
boehmes@33419
   665
      true
boehmes@33419
   666
fun-decl $ptr_eq 3 1
boehmes@33419
   667
    type-con $ptr 0
boehmes@33419
   668
    type-con $ptr 0
boehmes@33419
   669
    bool
boehmes@33419
   670
  attribute inline 1
boehmes@33419
   671
    expr-attr
boehmes@33419
   672
      true
boehmes@33419
   673
fun-decl $ptr_neq 3 1
boehmes@33419
   674
    type-con $ptr 0
boehmes@33419
   675
    type-con $ptr 0
boehmes@33419
   676
    bool
boehmes@33419
   677
  attribute inline 1
boehmes@33419
   678
    expr-attr
boehmes@33419
   679
      true
boehmes@33419
   680
fun-decl $is_primitive_field_of 4 1
boehmes@33419
   681
    type-con $state 0
boehmes@33419
   682
    type-con $ptr 0
boehmes@33419
   683
    type-con $ptr 0
boehmes@33419
   684
    bool
boehmes@33419
   685
  attribute inline 1
boehmes@33419
   686
    expr-attr
boehmes@33419
   687
      true
boehmes@33419
   688
fun-decl $instantiate_st 2 0
boehmes@33419
   689
    type-con $status 0
boehmes@33419
   690
    bool
boehmes@33419
   691
fun-decl $is_domain_root 3 0
boehmes@33419
   692
    type-con $state 0
boehmes@33419
   693
    type-con $ptr 0
boehmes@33419
   694
    bool
boehmes@33419
   695
fun-decl $in_wrapped_domain 3 0
boehmes@33419
   696
    type-con $state 0
boehmes@33419
   697
    type-con $ptr 0
boehmes@33419
   698
    bool
boehmes@33419
   699
fun-decl $thread_local_np 3 1
boehmes@33419
   700
    type-con $state 0
boehmes@33419
   701
    type-con $ptr 0
boehmes@33419
   702
    bool
boehmes@33419
   703
  attribute inline 1
boehmes@33419
   704
    expr-attr
boehmes@33419
   705
      true
boehmes@33419
   706
fun-decl $thread_local 3 0
boehmes@33419
   707
    type-con $state 0
boehmes@33419
   708
    type-con $ptr 0
boehmes@33419
   709
    bool
boehmes@33419
   710
fun-decl $thread_local2 4 1
boehmes@33419
   711
    type-con $state 0
boehmes@33419
   712
    type-con $ptr 0
boehmes@33419
   713
    type-con $ctype 0
boehmes@33419
   714
    bool
boehmes@33419
   715
  attribute inline 1
boehmes@33419
   716
    expr-attr
boehmes@33419
   717
      true
boehmes@33419
   718
fun-decl $dont_instantiate 2 0
boehmes@33419
   719
    type-con $ptr 0
boehmes@33419
   720
    bool
boehmes@33419
   721
fun-decl $dont_instantiate_int 2 0
boehmes@33419
   722
    int
boehmes@33419
   723
    bool
boehmes@33419
   724
fun-decl $dont_instantiate_state 2 0
boehmes@33419
   725
    type-con $state 0
boehmes@33419
   726
    bool
boehmes@33419
   727
fun-decl $instantiate_int 2 0
boehmes@33419
   728
    int
boehmes@33419
   729
    bool
boehmes@33419
   730
fun-decl $instantiate_bool 2 0
boehmes@33419
   731
    bool
boehmes@33419
   732
    bool
boehmes@33419
   733
fun-decl $instantiate_ptr 2 0
boehmes@33419
   734
    type-con $ptr 0
boehmes@33419
   735
    bool
boehmes@33419
   736
fun-decl $instantiate_ptrset 2 0
boehmes@33419
   737
    type-con $ptrset 0
boehmes@33419
   738
    bool
boehmes@33419
   739
fun-decl $inv 4 1
boehmes@33419
   740
    type-con $state 0
boehmes@33419
   741
    type-con $ptr 0
boehmes@33419
   742
    type-con $ctype 0
boehmes@33419
   743
    bool
boehmes@33419
   744
  attribute inline 1
boehmes@33419
   745
    expr-attr
boehmes@33419
   746
      true
boehmes@33419
   747
fun-decl $inv2nt 4 1
boehmes@33419
   748
    type-con $state 0
boehmes@33419
   749
    type-con $state 0
boehmes@33419
   750
    type-con $ptr 0
boehmes@33419
   751
    bool
boehmes@33419
   752
  attribute inline 1
boehmes@33419
   753
    expr-attr
boehmes@33419
   754
      true
boehmes@33419
   755
fun-decl $imply_inv 4 0
boehmes@33419
   756
    type-con $state 0
boehmes@33419
   757
    type-con $ptr 0
boehmes@33419
   758
    type-con $ctype 0
boehmes@33419
   759
    bool
boehmes@33419
   760
fun-decl $inv2 5 0
boehmes@33419
   761
    type-con $state 0
boehmes@33419
   762
    type-con $state 0
boehmes@33419
   763
    type-con $ptr 0
boehmes@33419
   764
    type-con $ctype 0
boehmes@33419
   765
    bool
boehmes@33419
   766
fun-decl $inv2_when_closed 5 1
boehmes@33419
   767
    type-con $state 0
boehmes@33419
   768
    type-con $state 0
boehmes@33419
   769
    type-con $ptr 0
boehmes@33419
   770
    type-con $ctype 0
boehmes@33419
   771
    bool
boehmes@33419
   772
  attribute inline 1
boehmes@33419
   773
    expr-attr
boehmes@33419
   774
      true
boehmes@33419
   775
fun-decl $sequential 5 1
boehmes@33419
   776
    type-con $state 0
boehmes@33419
   777
    type-con $state 0
boehmes@33419
   778
    type-con $ptr 0
boehmes@33419
   779
    type-con $ctype 0
boehmes@33419
   780
    bool
boehmes@33419
   781
  attribute weight 1
boehmes@33419
   782
    expr-attr
boehmes@33419
   783
      int-num 0
boehmes@33419
   784
fun-decl $depends 5 1
boehmes@33419
   785
    type-con $state 0
boehmes@33419
   786
    type-con $state 0
boehmes@33419
   787
    type-con $ptr 0
boehmes@33419
   788
    type-con $ptr 0
boehmes@33419
   789
    bool
boehmes@33419
   790
  attribute weight 1
boehmes@33419
   791
    expr-attr
boehmes@33419
   792
      int-num 0
boehmes@33419
   793
fun-decl $spans_the_same 5 1
boehmes@33419
   794
    type-con $state 0
boehmes@33419
   795
    type-con $state 0
boehmes@33419
   796
    type-con $ptr 0
boehmes@33419
   797
    type-con $ctype 0
boehmes@33419
   798
    bool
boehmes@33419
   799
  attribute weight 1
boehmes@33419
   800
    expr-attr
boehmes@33419
   801
      int-num 0
boehmes@33419
   802
fun-decl $state_spans_the_same 5 0
boehmes@33419
   803
    type-con $state 0
boehmes@33419
   804
    type-con $state 0
boehmes@33419
   805
    type-con $ptr 0
boehmes@33419
   806
    type-con $ctype 0
boehmes@33419
   807
    bool
boehmes@33419
   808
fun-decl $nonvolatile_spans_the_same 5 1
boehmes@33419
   809
    type-con $state 0
boehmes@33419
   810
    type-con $state 0
boehmes@33419
   811
    type-con $ptr 0
boehmes@33419
   812
    type-con $ctype 0
boehmes@33419
   813
    bool
boehmes@33419
   814
  attribute weight 1
boehmes@33419
   815
    expr-attr
boehmes@33419
   816
      int-num 0
boehmes@33419
   817
fun-decl $state_nonvolatile_spans_the_same 5 0
boehmes@33419
   818
    type-con $state 0
boehmes@33419
   819
    type-con $state 0
boehmes@33419
   820
    type-con $ptr 0
boehmes@33419
   821
    type-con $ctype 0
boehmes@33419
   822
    bool
boehmes@33419
   823
fun-decl $in_extent_of 4 1
boehmes@33419
   824
    type-con $state 0
boehmes@33419
   825
    type-con $ptr 0
boehmes@33419
   826
    type-con $ptr 0
boehmes@33419
   827
    bool
boehmes@33419
   828
  attribute inline 1
boehmes@33419
   829
    expr-attr
boehmes@33419
   830
      true
boehmes@33419
   831
fun-decl $in_full_extent_of 3 1
boehmes@33419
   832
    type-con $ptr 0
boehmes@33419
   833
    type-con $ptr 0
boehmes@33419
   834
    bool
boehmes@33419
   835
  attribute inline 1
boehmes@33419
   836
    expr-attr
boehmes@33419
   837
      true
boehmes@33419
   838
fun-decl $extent_mutable 3 0
boehmes@33419
   839
    type-con $state 0
boehmes@33419
   840
    type-con $ptr 0
boehmes@33419
   841
    bool
boehmes@33419
   842
fun-decl $extent_is_fresh 4 0
boehmes@33419
   843
    type-con $state 0
boehmes@33419
   844
    type-con $state 0
boehmes@33419
   845
    type-con $ptr 0
boehmes@33419
   846
    bool
boehmes@33419
   847
fun-decl $forall_inv2_when_closed 3 1
boehmes@33419
   848
    type-con $state 0
boehmes@33419
   849
    type-con $state 0
boehmes@33419
   850
    bool
boehmes@33419
   851
  attribute inline 1
boehmes@33419
   852
    expr-attr
boehmes@33419
   853
      true
boehmes@33419
   854
fun-decl $function_entry 2 0
boehmes@33419
   855
    type-con $state 0
boehmes@33419
   856
    bool
boehmes@33419
   857
fun-decl $full_stop 2 0
boehmes@33419
   858
    type-con $state 0
boehmes@33419
   859
    bool
boehmes@33419
   860
fun-decl $full_stop_ext 3 1
boehmes@33419
   861
    type-con $token 0
boehmes@33419
   862
    type-con $state 0
boehmes@33419
   863
    bool
boehmes@33419
   864
  attribute inline 1
boehmes@33419
   865
    expr-attr
boehmes@33419
   866
      true
boehmes@33419
   867
fun-decl $file_name_is 3 0
boehmes@33419
   868
    int
boehmes@33419
   869
    type-con $token 0
boehmes@33419
   870
    bool
boehmes@33419
   871
fun-decl $closed_is_transitive 2 1
boehmes@33419
   872
    type-con $state 0
boehmes@33419
   873
    bool
boehmes@33419
   874
  attribute inline 1
boehmes@33419
   875
    expr-attr
boehmes@33419
   876
      true
boehmes@33419
   877
fun-decl $call_transition 3 0
boehmes@33419
   878
    type-con $state 0
boehmes@33419
   879
    type-con $state 0
boehmes@33419
   880
    bool
boehmes@33419
   881
fun-decl $good_state_ext 3 0
boehmes@33419
   882
    type-con $token 0
boehmes@33419
   883
    type-con $state 0
boehmes@33419
   884
    bool
boehmes@33419
   885
fun-decl $local_value_is 6 0
boehmes@33419
   886
    type-con $state 0
boehmes@33419
   887
    type-con $token 0
boehmes@33419
   888
    type-con $token 0
boehmes@33419
   889
    int
boehmes@33419
   890
    type-con $ctype 0
boehmes@33419
   891
    bool
boehmes@33419
   892
fun-decl $local_value_is_ptr 6 0
boehmes@33419
   893
    type-con $state 0
boehmes@33419
   894
    type-con $token 0
boehmes@33419
   895
    type-con $token 0
boehmes@33419
   896
    type-con $ptr 0
boehmes@33419
   897
    type-con $ctype 0
boehmes@33419
   898
    bool
boehmes@33419
   899
fun-decl $read_ptr_m 4 0
boehmes@33419
   900
    type-con $state 0
boehmes@33419
   901
    type-con $ptr 0
boehmes@33419
   902
    type-con $ctype 0
boehmes@33419
   903
    type-con $ptr 0
boehmes@33419
   904
fun-decl $type_code_is 3 0
boehmes@33419
   905
    int
boehmes@33419
   906
    type-con $ctype 0
boehmes@33419
   907
    bool
boehmes@33419
   908
fun-decl $function_arg_type 4 0
boehmes@33419
   909
    type-con $pure_function 0
boehmes@33419
   910
    int
boehmes@33419
   911
    type-con $ctype 0
boehmes@33419
   912
    bool
boehmes@33419
   913
fun-decl $ver_domain 2 0
boehmes@33419
   914
    type-con $version 0
boehmes@33419
   915
    type-con $ptrset 0
boehmes@33419
   916
fun-decl $read_version 3 1
boehmes@33419
   917
    type-con $state 0
boehmes@33419
   918
    type-con $ptr 0
boehmes@33419
   919
    type-con $version 0
boehmes@33419
   920
  attribute weight 1
boehmes@33419
   921
    expr-attr
boehmes@33419
   922
      int-num 0
boehmes@33419
   923
fun-decl $domain 3 1
boehmes@33419
   924
    type-con $state 0
boehmes@33419
   925
    type-con $ptr 0
boehmes@33419
   926
    type-con $ptrset 0
boehmes@33419
   927
  attribute weight 1
boehmes@33419
   928
    expr-attr
boehmes@33419
   929
      int-num 0
boehmes@33419
   930
fun-decl $in_domain 4 0
boehmes@33419
   931
    type-con $state 0
boehmes@33419
   932
    type-con $ptr 0
boehmes@33419
   933
    type-con $ptr 0
boehmes@33419
   934
    bool
boehmes@33419
   935
fun-decl $in_vdomain 4 0
boehmes@33419
   936
    type-con $state 0
boehmes@33419
   937
    type-con $ptr 0
boehmes@33419
   938
    type-con $ptr 0
boehmes@33419
   939
    bool
boehmes@33419
   940
fun-decl $in_domain_lab 5 0
boehmes@33419
   941
    type-con $state 0
boehmes@33419
   942
    type-con $ptr 0
boehmes@33419
   943
    type-con $ptr 0
boehmes@33419
   944
    type-con $label 0
boehmes@33419
   945
    bool
boehmes@33419
   946
fun-decl $in_vdomain_lab 5 0
boehmes@33419
   947
    type-con $state 0
boehmes@33419
   948
    type-con $ptr 0
boehmes@33419
   949
    type-con $ptr 0
boehmes@33419
   950
    type-con $label 0
boehmes@33419
   951
    bool
boehmes@33419
   952
fun-decl $inv_lab 4 0
boehmes@33419
   953
    type-con $state 0
boehmes@33419
   954
    type-con $ptr 0
boehmes@33419
   955
    type-con $label 0
boehmes@33419
   956
    bool
boehmes@33419
   957
fun-decl $dom_thread_local 3 1
boehmes@33419
   958
    type-con $state 0
boehmes@33419
   959
    type-con $ptr 0
boehmes@33419
   960
    bool
boehmes@33419
   961
  attribute inline 1
boehmes@33419
   962
    expr-attr
boehmes@33419
   963
      true
boehmes@33419
   964
fun-decl $fetch_from_domain 3 0
boehmes@33419
   965
    type-con $version 0
boehmes@33419
   966
    type-con $ptr 0
boehmes@33419
   967
    int
boehmes@33419
   968
fun-decl $in_claim_domain 3 0
boehmes@33419
   969
    type-con $ptr 0
boehmes@33419
   970
    type-con $ptr 0
boehmes@33419
   971
    bool
boehmes@33419
   972
fun-decl $by_claim 5 1
boehmes@33419
   973
    type-con $state 0
boehmes@33419
   974
    type-con $ptr 0
boehmes@33419
   975
    type-con $ptr 0
boehmes@33419
   976
    type-con $ptr 0
boehmes@33419
   977
    type-con $ptr 0
boehmes@33419
   978
  attribute weight 1
boehmes@33419
   979
    expr-attr
boehmes@33419
   980
      int-num 0
boehmes@33419
   981
fun-decl $claim_version 2 0
boehmes@33419
   982
    type-con $ptr 0
boehmes@33419
   983
    type-con $version 0
boehmes@33419
   984
fun-decl $read_vol_version 3 1
boehmes@33419
   985
    type-con $state 0
boehmes@33419
   986
    type-con $ptr 0
boehmes@33419
   987
    type-con $vol_version 0
boehmes@33419
   988
  attribute weight 1
boehmes@33419
   989
    expr-attr
boehmes@33419
   990
      int-num 0
boehmes@33419
   991
fun-decl $fetch_from_vv 3 0
boehmes@33419
   992
    type-con $vol_version 0
boehmes@33419
   993
    type-con $ptr 0
boehmes@33419
   994
    int
boehmes@33419
   995
fun-decl $fetch_vol_field 4 1
boehmes@33419
   996
    type-con $state 0
boehmes@33419
   997
    type-con $ptr 0
boehmes@33419
   998
    type-con $field 0
boehmes@33419
   999
    int
boehmes@33419
  1000
  attribute inline 1
boehmes@33419
  1001
    expr-attr
boehmes@33419
  1002
      true
boehmes@33419
  1003
fun-decl $is_approved_by 4 0
boehmes@33419
  1004
    type-con $ctype 0
boehmes@33419
  1005
    type-con $field 0
boehmes@33419
  1006
    type-con $field 0
boehmes@33419
  1007
    bool
boehmes@33419
  1008
fun-decl $inv_is_approved_by_ptr 6 1
boehmes@33419
  1009
    type-con $state 0
boehmes@33419
  1010
    type-con $state 0
boehmes@33419
  1011
    type-con $ptr 0
boehmes@33419
  1012
    type-con $ptr 0
boehmes@33419
  1013
    type-con $field 0
boehmes@33419
  1014
    bool
boehmes@33419
  1015
  attribute inline 1
boehmes@33419
  1016
    expr-attr
boehmes@33419
  1017
      true
boehmes@33419
  1018
fun-decl $inv_is_approved_by 6 1
boehmes@33419
  1019
    type-con $state 0
boehmes@33419
  1020
    type-con $state 0
boehmes@33419
  1021
    type-con $ptr 0
boehmes@33419
  1022
    type-con $field 0
boehmes@33419
  1023
    type-con $field 0
boehmes@33419
  1024
    bool
boehmes@33419
  1025
  attribute inline 1
boehmes@33419
  1026
    expr-attr
boehmes@33419
  1027
      true
boehmes@33419
  1028
fun-decl $is_owner_approved 3 0
boehmes@33419
  1029
    type-con $ctype 0
boehmes@33419
  1030
    type-con $field 0
boehmes@33419
  1031
    bool
boehmes@33419
  1032
fun-decl $inv_is_owner_approved 5 1
boehmes@33419
  1033
    type-con $state 0
boehmes@33419
  1034
    type-con $state 0
boehmes@33419
  1035
    type-con $ptr 0
boehmes@33419
  1036
    type-con $field 0
boehmes@33419
  1037
    bool
boehmes@33419
  1038
  attribute inline 1
boehmes@33419
  1039
    expr-attr
boehmes@33419
  1040
      true
boehmes@33419
  1041
fun-decl $good_for_admissibility 2 0
boehmes@33419
  1042
    type-con $state 0
boehmes@33419
  1043
    bool
boehmes@33419
  1044
fun-decl $good_for_post_admissibility 2 0
boehmes@33419
  1045
    type-con $state 0
boehmes@33419
  1046
    bool
boehmes@33419
  1047
fun-decl $stuttering_pre 3 1
boehmes@33419
  1048
    type-con $state 0
boehmes@33419
  1049
    type-con $ptr 0
boehmes@33419
  1050
    bool
boehmes@33419
  1051
  attribute inline 1
boehmes@33419
  1052
    expr-attr
boehmes@33419
  1053
      true
boehmes@33419
  1054
fun-decl $admissibility_pre 3 1
boehmes@33419
  1055
    type-con $state 0
boehmes@33419
  1056
    type-con $ptr 0
boehmes@33419
  1057
    bool
boehmes@33419
  1058
  attribute inline 1
boehmes@33419
  1059
    expr-attr
boehmes@33419
  1060
      true
boehmes@33419
  1061
fun-decl $mutable_increases 3 1
boehmes@33419
  1062
    type-con $state 0
boehmes@33419
  1063
    type-con $state 0
boehmes@33419
  1064
    bool
boehmes@33419
  1065
  attribute inline 1
boehmes@33419
  1066
    expr-attr
boehmes@33419
  1067
      true
boehmes@33419
  1068
fun-decl $meta_eq 3 1
boehmes@33419
  1069
    type-con $state 0
boehmes@33419
  1070
    type-con $state 0
boehmes@33419
  1071
    bool
boehmes@33419
  1072
  attribute inline 1
boehmes@33419
  1073
    expr-attr
boehmes@33419
  1074
      true
boehmes@33419
  1075
fun-decl $is_stuttering_check 1 0
boehmes@33419
  1076
    bool
boehmes@33419
  1077
fun-decl $is_unwrap_check 1 0
boehmes@33419
  1078
    bool
boehmes@33419
  1079
fun-decl $is_admissibility_check 1 1
boehmes@33419
  1080
    bool
boehmes@33419
  1081
  attribute inline 1
boehmes@33419
  1082
    expr-attr
boehmes@33419
  1083
      true
boehmes@33419
  1084
fun-decl $good_for_pre_can_unwrap 2 0
boehmes@33419
  1085
    type-con $state 0
boehmes@33419
  1086
    bool
boehmes@33419
  1087
fun-decl $good_for_post_can_unwrap 2 0
boehmes@33419
  1088
    type-con $state 0
boehmes@33419
  1089
    bool
boehmes@33419
  1090
fun-decl $unwrap_check_pre 3 1
boehmes@33419
  1091
    type-con $state 0
boehmes@33419
  1092
    type-con $ptr 0
boehmes@33419
  1093
    bool
boehmes@33419
  1094
  attribute inline 1
boehmes@33419
  1095
    expr-attr
boehmes@33419
  1096
      true
boehmes@33419
  1097
fun-decl $update_int 4 0
boehmes@33419
  1098
    type-con $state 0
boehmes@33419
  1099
    type-con $ptr 0
boehmes@33419
  1100
    int
boehmes@33419
  1101
    type-con $state 0
boehmes@33419
  1102
fun-decl $timestamp_is_now 3 1
boehmes@33419
  1103
    type-con $state 0
boehmes@33419
  1104
    type-con $ptr 0
boehmes@33419
  1105
    bool
boehmes@33419
  1106
  attribute inline 1
boehmes@33419
  1107
    expr-attr
boehmes@33419
  1108
      true
boehmes@33419
  1109
fun-decl $now_writable 3 1
boehmes@33419
  1110
    type-con $state 0
boehmes@33419
  1111
    type-con $ptr 0
boehmes@33419
  1112
    bool
boehmes@33419
  1113
  attribute inline 1
boehmes@33419
  1114
    expr-attr
boehmes@33419
  1115
      true
boehmes@33419
  1116
fun-decl $timestamp_post 3 1
boehmes@33419
  1117
    type-con $state 0
boehmes@33419
  1118
    type-con $state 0
boehmes@33419
  1119
    bool
boehmes@33419
  1120
  attribute inline 1
boehmes@33419
  1121
    expr-attr
boehmes@33419
  1122
      true
boehmes@33419
  1123
fun-decl $timestamp_post_strict 3 1
boehmes@33419
  1124
    type-con $state 0
boehmes@33419
  1125
    type-con $state 0
boehmes@33419
  1126
    bool
boehmes@33419
  1127
  attribute inline 1
boehmes@33419
  1128
    expr-attr
boehmes@33419
  1129
      true
boehmes@33419
  1130
fun-decl $pre_wrap 2 0
boehmes@33419
  1131
    type-con $state 0
boehmes@33419
  1132
    bool
boehmes@33419
  1133
fun-decl $pre_unwrap 2 0
boehmes@33419
  1134
    type-con $state 0
boehmes@33419
  1135
    bool
boehmes@33419
  1136
fun-decl $pre_static_wrap 2 0
boehmes@33419
  1137
    type-con $state 0
boehmes@33419
  1138
    bool
boehmes@33419
  1139
fun-decl $pre_static_unwrap 2 0
boehmes@33419
  1140
    type-con $state 0
boehmes@33419
  1141
    bool
boehmes@33419
  1142
fun-decl $unwrap_post 5 1
boehmes@33419
  1143
    type-con $state 0
boehmes@33419
  1144
    type-con $state 0
boehmes@33419
  1145
    type-con $ptr 0
boehmes@33419
  1146
    type-con $ptr 0
boehmes@33419
  1147
    bool
boehmes@33419
  1148
  attribute inline 1
boehmes@33419
  1149
    expr-attr
boehmes@33419
  1150
      true
boehmes@33419
  1151
fun-decl $unwrap_post_claimable 5 1
boehmes@33419
  1152
    type-con $state 0
boehmes@33419
  1153
    type-con $state 0
boehmes@33419
  1154
    type-con $ptr 0
boehmes@33419
  1155
    type-con $ptr 0
boehmes@33419
  1156
    bool
boehmes@33419
  1157
  attribute inline 1
boehmes@33419
  1158
    expr-attr
boehmes@33419
  1159
      true
boehmes@33419
  1160
fun-decl $keeps 4 2
boehmes@33419
  1161
    type-con $state 0
boehmes@33419
  1162
    type-con $ptr 0
boehmes@33419
  1163
    type-con $ptr 0
boehmes@33419
  1164
    bool
boehmes@33419
  1165
  attribute inline 1
boehmes@33419
  1166
    expr-attr
boehmes@33419
  1167
      true
boehmes@33419
  1168
  attribute expand 1
boehmes@33419
  1169
    expr-attr
boehmes@33419
  1170
      true
boehmes@33419
  1171
fun-decl $expect_unreachable 1 0
boehmes@33419
  1172
    bool
boehmes@33419
  1173
fun-decl $taken_over 4 0
boehmes@33419
  1174
    type-con $state 0
boehmes@33419
  1175
    type-con $ptr 0
boehmes@33419
  1176
    type-con $ptr 0
boehmes@33419
  1177
    type-con $status 0
boehmes@33419
  1178
fun-decl $take_over 4 0
boehmes@33419
  1179
    type-con $state 0
boehmes@33419
  1180
    type-con $ptr 0
boehmes@33419
  1181
    type-con $ptr 0
boehmes@33419
  1182
    type-con $state 0
boehmes@33419
  1183
fun-decl $released 4 0
boehmes@33419
  1184
    type-con $state 0
boehmes@33419
  1185
    type-con $ptr 0
boehmes@33419
  1186
    type-con $ptr 0
boehmes@33419
  1187
    type-con $status 0
boehmes@33419
  1188
fun-decl $release 5 0
boehmes@33419
  1189
    type-con $state 0
boehmes@33419
  1190
    type-con $state 0
boehmes@33419
  1191
    type-con $ptr 0
boehmes@33419
  1192
    type-con $ptr 0
boehmes@33419
  1193
    type-con $state 0
boehmes@33419
  1194
fun-decl $post_unwrap 3 0
boehmes@33419
  1195
    type-con $state 0
boehmes@33419
  1196
    type-con $state 0
boehmes@33419
  1197
    bool
boehmes@33419
  1198
fun-decl $new_ownees 4 1
boehmes@33419
  1199
    type-con $state 0
boehmes@33419
  1200
    type-con $ptr 0
boehmes@33419
  1201
    type-con $ptrset 0
boehmes@33419
  1202
    type-con $ptrset 0
boehmes@33419
  1203
  attribute inline 1
boehmes@33419
  1204
    expr-attr
boehmes@33419
  1205
      true
boehmes@33419
  1206
fun-decl $get_memory_allocator 1 0
boehmes@33419
  1207
    type-con $ptr 0
boehmes@33419
  1208
fun-decl $memory_allocator_type 1 1
boehmes@33419
  1209
    type-con $ctype 0
boehmes@33419
  1210
  attribute unique 0
boehmes@33419
  1211
fun-decl $memory_allocator_ref 1 0
boehmes@33419
  1212
    int
boehmes@33419
  1213
fun-decl $program_entry_point 2 0
boehmes@33419
  1214
    type-con $state 0
boehmes@33419
  1215
    bool
boehmes@33419
  1216
fun-decl $program_entry_point_ch 2 0
boehmes@33419
  1217
    type-con $state 0
boehmes@33419
  1218
    bool
boehmes@33419
  1219
fun-decl $is_global 3 1
boehmes@33419
  1220
    type-con $ptr 0
boehmes@33419
  1221
    type-con $ctype 0
boehmes@33419
  1222
    bool
boehmes@33419
  1223
  attribute inline 1
boehmes@33419
  1224
    expr-attr
boehmes@33419
  1225
      true
boehmes@33419
  1226
fun-decl $is_global_array 4 1
boehmes@33419
  1227
    type-con $ptr 0
boehmes@33419
  1228
    type-con $ctype 0
boehmes@33419
  1229
    int
boehmes@33419
  1230
    bool
boehmes@33419
  1231
  attribute inline 1
boehmes@33419
  1232
    expr-attr
boehmes@33419
  1233
      true
boehmes@33419
  1234
fun-decl $active_option 3 1
boehmes@33419
  1235
    type-con $state 0
boehmes@33419
  1236
    type-con $ptr 0
boehmes@33419
  1237
    type-con $field 0
boehmes@33419
  1238
  attribute inline 1
boehmes@33419
  1239
    expr-attr
boehmes@33419
  1240
      true
boehmes@33419
  1241
fun-decl $ts_active_option 2 0
boehmes@33419
  1242
    type-con $type_state 0
boehmes@33419
  1243
    type-con $field 0
boehmes@33419
  1244
fun-decl $union_active 4 1
boehmes@33419
  1245
    type-con $state 0
boehmes@33419
  1246
    type-con $ptr 0
boehmes@33419
  1247
    type-con $field 0
boehmes@33419
  1248
    bool
boehmes@33419
  1249
  attribute inline 1
boehmes@33419
  1250
    expr-attr
boehmes@33419
  1251
      true
boehmes@33419
  1252
fun-decl $is_union_field 3 0
boehmes@33419
  1253
    type-con $ctype 0
boehmes@33419
  1254
    type-con $field 0
boehmes@33419
  1255
    bool
boehmes@33419
  1256
fun-decl $union_havoced 4 1
boehmes@33419
  1257
    type-con $state 0
boehmes@33419
  1258
    type-con $state 0
boehmes@33419
  1259
    type-con $ptr 0
boehmes@33419
  1260
    bool
boehmes@33419
  1261
  attribute inline 1
boehmes@33419
  1262
    expr-attr
boehmes@33419
  1263
      true
boehmes@33419
  1264
fun-decl $full_extent 2 0
boehmes@33419
  1265
    type-con $ptr 0
boehmes@33419
  1266
    type-con $ptrset 0
boehmes@33419
  1267
fun-decl $extent 3 0
boehmes@33419
  1268
    type-con $state 0
boehmes@33419
  1269
    type-con $ptr 0
boehmes@33419
  1270
    type-con $ptrset 0
boehmes@33419
  1271
fun-decl $span 2 0
boehmes@33419
  1272
    type-con $ptr 0
boehmes@33419
  1273
    type-con $ptrset 0
boehmes@33419
  1274
fun-decl $in_span_of 3 1
boehmes@33419
  1275
    type-con $ptr 0
boehmes@33419
  1276
    type-con $ptr 0
boehmes@33419
  1277
    bool
boehmes@33419
  1278
  attribute inline 1
boehmes@33419
  1279
    expr-attr
boehmes@33419
  1280
      true
boehmes@33419
  1281
fun-decl $first_option_typed 3 0
boehmes@33419
  1282
    type-con $state 0
boehmes@33419
  1283
    type-con $ptr 0
boehmes@33419
  1284
    bool
boehmes@33419
  1285
fun-decl $struct_extent 2 1
boehmes@33419
  1286
    type-con $ptr 0
boehmes@33419
  1287
    type-con $ptrset 0
boehmes@33419
  1288
  attribute inline 1
boehmes@33419
  1289
    expr-attr
boehmes@33419
  1290
      true
boehmes@33419
  1291
fun-decl $in_struct_extent_of 3 1
boehmes@33419
  1292
    type-con $ptr 0
boehmes@33419
  1293
    type-con $ptr 0
boehmes@33419
  1294
    bool
boehmes@33419
  1295
  attribute inline 1
boehmes@33419
  1296
    expr-attr
boehmes@33419
  1297
      true
boehmes@33419
  1298
fun-decl $volatile_span 3 0
boehmes@33419
  1299
    type-con $state 0
boehmes@33419
  1300
    type-con $ptr 0
boehmes@33419
  1301
    type-con $ptrset 0
boehmes@33419
  1302
fun-decl $left_split 3 0
boehmes@33419
  1303
    type-con $ptr 0
boehmes@33419
  1304
    int
boehmes@33419
  1305
    type-con $ptr 0
boehmes@33419
  1306
fun-decl $right_split 3 0
boehmes@33419
  1307
    type-con $ptr 0
boehmes@33419
  1308
    int
boehmes@33419
  1309
    type-con $ptr 0
boehmes@33419
  1310
fun-decl $joined_array 3 0
boehmes@33419
  1311
    type-con $ptr 0
boehmes@33419
  1312
    type-con $ptr 0
boehmes@33419
  1313
    type-con $ptr 0
boehmes@33419
  1314
fun-decl $mutable_root 3 1
boehmes@33419
  1315
    type-con $state 0
boehmes@33419
  1316
    type-con $ptr 0
boehmes@33419
  1317
    bool
boehmes@33419
  1318
  attribute inline 1
boehmes@33419
  1319
    expr-attr
boehmes@33419
  1320
      true
boehmes@33419
  1321
fun-decl $set_in 3 0
boehmes@33419
  1322
    type-con $ptr 0
boehmes@33419
  1323
    type-con $ptrset 0
boehmes@33419
  1324
    bool
boehmes@33419
  1325
fun-decl $set_empty 1 0
boehmes@33419
  1326
    type-con $ptrset 0
boehmes@33419
  1327
fun-decl $set_singleton 2 0
boehmes@33419
  1328
    type-con $ptr 0
boehmes@33419
  1329
    type-con $ptrset 0
boehmes@33419
  1330
fun-decl $non_null_set_singleton 2 0
boehmes@33419
  1331
    type-con $ptr 0
boehmes@33419
  1332
    type-con $ptrset 0
boehmes@33419
  1333
fun-decl $set_union 3 0
boehmes@33419
  1334
    type-con $ptrset 0
boehmes@33419
  1335
    type-con $ptrset 0
boehmes@33419
  1336
    type-con $ptrset 0
boehmes@33419
  1337
fun-decl $set_difference 3 0
boehmes@33419
  1338
    type-con $ptrset 0
boehmes@33419
  1339
    type-con $ptrset 0
boehmes@33419
  1340
    type-con $ptrset 0
boehmes@33419
  1341
fun-decl $set_intersection 3 0
boehmes@33419
  1342
    type-con $ptrset 0
boehmes@33419
  1343
    type-con $ptrset 0
boehmes@33419
  1344
    type-con $ptrset 0
boehmes@33419
  1345
fun-decl $set_subset 3 0
boehmes@33419
  1346
    type-con $ptrset 0
boehmes@33419
  1347
    type-con $ptrset 0
boehmes@33419
  1348
    bool
boehmes@33419
  1349
fun-decl $set_eq 3 0
boehmes@33419
  1350
    type-con $ptrset 0
boehmes@33419
  1351
    type-con $ptrset 0
boehmes@33419
  1352
    bool
boehmes@33419
  1353
fun-decl $set_cardinality 2 0
boehmes@33419
  1354
    type-con $ptrset 0
boehmes@33419
  1355
    int
boehmes@33419
  1356
fun-decl $set_universe 1 0
boehmes@33419
  1357
    type-con $ptrset 0
boehmes@33419
  1358
fun-decl $set_disjoint 3 0
boehmes@33419
  1359
    type-con $ptrset 0
boehmes@33419
  1360
    type-con $ptrset 0
boehmes@33419
  1361
    bool
boehmes@33419
  1362
fun-decl $id_set_disjoint 4 0
boehmes@33419
  1363
    type-con $ptr 0
boehmes@33419
  1364
    type-con $ptrset 0
boehmes@33419
  1365
    type-con $ptrset 0
boehmes@33419
  1366
    int
boehmes@33419
  1367
fun-decl $set_in3 3 0
boehmes@33419
  1368
    type-con $ptr 0
boehmes@33419
  1369
    type-con $ptrset 0
boehmes@33419
  1370
    bool
boehmes@33419
  1371
fun-decl $set_in2 3 0
boehmes@33419
  1372
    type-con $ptr 0
boehmes@33419
  1373
    type-con $ptrset 0
boehmes@33419
  1374
    bool
boehmes@33419
  1375
fun-decl $in_some_owns 2 0
boehmes@33419
  1376
    type-con $ptr 0
boehmes@33419
  1377
    bool
boehmes@33419
  1378
fun-decl $set_in0 3 0
boehmes@33419
  1379
    type-con $ptr 0
boehmes@33419
  1380
    type-con $ptrset 0
boehmes@33419
  1381
    bool
boehmes@33419
  1382
fun-decl sk_hack 2 0
boehmes@33419
  1383
    bool
boehmes@33419
  1384
    bool
boehmes@33419
  1385
fun-decl $writes_nothing 3 1
boehmes@33419
  1386
    type-con $state 0
boehmes@33419
  1387
    type-con $state 0
boehmes@33419
  1388
    bool
boehmes@33419
  1389
  attribute inline 1
boehmes@33419
  1390
    expr-attr
boehmes@33419
  1391
      true
boehmes@33419
  1392
fun-decl $array 3 0
boehmes@33419
  1393
    type-con $ctype 0
boehmes@33419
  1394
    int
boehmes@33419
  1395
    type-con $ctype 0
boehmes@33419
  1396
fun-decl $element_type 2 0
boehmes@33419
  1397
    type-con $ctype 0
boehmes@33419
  1398
    type-con $ctype 0
boehmes@33419
  1399
fun-decl $array_length 2 0
boehmes@33419
  1400
    type-con $ctype 0
boehmes@33419
  1401
    int
boehmes@33419
  1402
fun-decl $is_array_elt 3 1
boehmes@33419
  1403
    type-con $state 0
boehmes@33419
  1404
    type-con $ptr 0
boehmes@33419
  1405
    bool
boehmes@33419
  1406
  attribute inline 1
boehmes@33419
  1407
    expr-attr
boehmes@33419
  1408
      true
boehmes@33419
  1409
fun-decl $inlined_array 3 1
boehmes@33419
  1410
    type-con $ptr 0
boehmes@33419
  1411
    type-con $ctype 0
boehmes@33419
  1412
    type-con $ptr 0
boehmes@33419
  1413
  attribute weight 1
boehmes@33419
  1414
    expr-attr
boehmes@33419
  1415
      int-num 0
boehmes@33419
  1416
fun-decl $idx 4 0
boehmes@33419
  1417
    type-con $ptr 0
boehmes@33419
  1418
    int
boehmes@33419
  1419
    type-con $ctype 0
boehmes@33419
  1420
    type-con $ptr 0
boehmes@33419
  1421
fun-decl $add.mul 4 2
boehmes@33419
  1422
    int
boehmes@33419
  1423
    int
boehmes@33419
  1424
    int
boehmes@33419
  1425
    int
boehmes@33419
  1426
  attribute inline 1
boehmes@33419
  1427
    expr-attr
boehmes@33419
  1428
      true
boehmes@33419
  1429
  attribute expand 1
boehmes@33419
  1430
    expr-attr
boehmes@33419
  1431
      true
boehmes@33419
  1432
fun-decl $add 3 2
boehmes@33419
  1433
    int
boehmes@33419
  1434
    int
boehmes@33419
  1435
    int
boehmes@33419
  1436
  attribute inline 1
boehmes@33419
  1437
    expr-attr
boehmes@33419
  1438
      true
boehmes@33419
  1439
  attribute expand 1
boehmes@33419
  1440
    expr-attr
boehmes@33419
  1441
      true
boehmes@33419
  1442
fun-decl $is_array_vol_or_nonvol 6 1
boehmes@33419
  1443
    type-con $state 0
boehmes@33419
  1444
    type-con $ptr 0
boehmes@33419
  1445
    type-con $ctype 0
boehmes@33419
  1446
    int
boehmes@33419
  1447
    bool
boehmes@33419
  1448
    bool
boehmes@33419
  1449
  attribute weight 1
boehmes@33419
  1450
    expr-attr
boehmes@33419
  1451
      int-num 0
boehmes@33419
  1452
fun-decl $is_array 5 1
boehmes@33419
  1453
    type-con $state 0
boehmes@33419
  1454
    type-con $ptr 0
boehmes@33419
  1455
    type-con $ctype 0
boehmes@33419
  1456
    int
boehmes@33419
  1457
    bool
boehmes@33419
  1458
  attribute weight 1
boehmes@33419
  1459
    expr-attr
boehmes@33419
  1460
      int-num 0
boehmes@33419
  1461
fun-decl $is_thread_local_array 5 1
boehmes@33419
  1462
    type-con $state 0
boehmes@33419
  1463
    type-con $ptr 0
boehmes@33419
  1464
    type-con $ctype 0
boehmes@33419
  1465
    int
boehmes@33419
  1466
    bool
boehmes@33419
  1467
  attribute inline 1
boehmes@33419
  1468
    expr-attr
boehmes@33419
  1469
      true
boehmes@33419
  1470
fun-decl $is_mutable_array 5 1
boehmes@33419
  1471
    type-con $state 0
boehmes@33419
  1472
    type-con $ptr 0
boehmes@33419
  1473
    type-con $ctype 0
boehmes@33419
  1474
    int
boehmes@33419
  1475
    bool
boehmes@33419
  1476
  attribute inline 1
boehmes@33419
  1477
    expr-attr
boehmes@33419
  1478
      true
boehmes@33419
  1479
fun-decl $is_array_emb 6 1
boehmes@33419
  1480
    type-con $state 0
boehmes@33419
  1481
    type-con $ptr 0
boehmes@33419
  1482
    type-con $ctype 0
boehmes@33419
  1483
    int
boehmes@33419
  1484
    type-con $ptr 0
boehmes@33419
  1485
    bool
boehmes@33419
  1486
  attribute inline 1
boehmes@33419
  1487
    expr-attr
boehmes@33419
  1488
      true
boehmes@33419
  1489
fun-decl $is_array_emb_path 8 1
boehmes@33419
  1490
    type-con $state 0
boehmes@33419
  1491
    type-con $ptr 0
boehmes@33419
  1492
    type-con $ctype 0
boehmes@33419
  1493
    int
boehmes@33419
  1494
    type-con $ptr 0
boehmes@33419
  1495
    type-con $field 0
boehmes@33419
  1496
    bool
boehmes@33419
  1497
    bool
boehmes@33419
  1498
  attribute inline 1
boehmes@33419
  1499
    expr-attr
boehmes@33419
  1500
      true
boehmes@33419
  1501
fun-decl $array_field_properties 6 1
boehmes@33419
  1502
    type-con $field 0
boehmes@33419
  1503
    type-con $ctype 0
boehmes@33419
  1504
    int
boehmes@33419
  1505
    bool
boehmes@33419
  1506
    bool
boehmes@33419
  1507
    bool
boehmes@33419
  1508
  attribute inline 1
boehmes@33419
  1509
    expr-attr
boehmes@33419
  1510
      true
boehmes@33419
  1511
fun-decl $no_inline_array_field_properties 6 1
boehmes@33419
  1512
    type-con $field 0
boehmes@33419
  1513
    type-con $ctype 0
boehmes@33419
  1514
    int
boehmes@33419
  1515
    bool
boehmes@33419
  1516
    bool
boehmes@33419
  1517
    bool
boehmes@33419
  1518
  attribute inline 1
boehmes@33419
  1519
    expr-attr
boehmes@33419
  1520
      true
boehmes@33419
  1521
fun-decl $array_elt_emb 4 1
boehmes@33419
  1522
    type-con $state 0
boehmes@33419
  1523
    type-con $ptr 0
boehmes@33419
  1524
    type-con $ptr 0
boehmes@33419
  1525
    bool
boehmes@33419
  1526
  attribute inline 1
boehmes@33419
  1527
    expr-attr
boehmes@33419
  1528
      true
boehmes@33419
  1529
fun-decl $array_members 4 0
boehmes@33419
  1530
    type-con $ptr 0
boehmes@33419
  1531
    type-con $ctype 0
boehmes@33419
  1532
    int
boehmes@33419
  1533
    type-con $ptrset 0
boehmes@33419
  1534
fun-decl $array_range 4 0
boehmes@33419
  1535
    type-con $ptr 0
boehmes@33419
  1536
    type-con $ctype 0
boehmes@33419
  1537
    int
boehmes@33419
  1538
    type-con $ptrset 0
boehmes@33419
  1539
fun-decl $non_null_array_range 4 0
boehmes@33419
  1540
    type-con $ptr 0
boehmes@33419
  1541
    type-con $ctype 0
boehmes@33419
  1542
    int
boehmes@33419
  1543
    type-con $ptrset 0
boehmes@33419
  1544
fun-decl $non_null_extent 3 0
boehmes@33419
  1545
    type-con $state 0
boehmes@33419
  1546
    type-con $ptr 0
boehmes@33419
  1547
    type-con $ptrset 0
boehmes@33419
  1548
fun-decl $as_array 4 1
boehmes@33419
  1549
    type-con $ptr 0
boehmes@33419
  1550
    type-con $ctype 0
boehmes@33419
  1551
    int
boehmes@33419
  1552
    type-con $ptr 0
boehmes@33419
  1553
  attribute inline 1
boehmes@33419
  1554
    expr-attr
boehmes@33419
  1555
      true
boehmes@33419
  1556
fun-decl $array_eq 6 1
boehmes@33419
  1557
    type-con $state 0
boehmes@33419
  1558
    type-con $state 0
boehmes@33419
  1559
    type-con $ptr 0
boehmes@33419
  1560
    type-con $ctype 0
boehmes@33419
  1561
    int
boehmes@33419
  1562
    bool
boehmes@33419
  1563
  attribute inline 1
boehmes@33419
  1564
    expr-attr
boehmes@33419
  1565
      true
boehmes@33419
  1566
fun-decl $index_within 3 0
boehmes@33419
  1567
    type-con $ptr 0
boehmes@33419
  1568
    type-con $ptr 0
boehmes@33419
  1569
    int
boehmes@33419
  1570
fun-decl $in_array 5 1
boehmes@33419
  1571
    type-con $ptr 0
boehmes@33419
  1572
    type-con $ptr 0
boehmes@33419
  1573
    type-con $ctype 0
boehmes@33419
  1574
    int
boehmes@33419
  1575
    bool
boehmes@33419
  1576
  attribute inline 1
boehmes@33419
  1577
    expr-attr
boehmes@33419
  1578
      true
boehmes@33419
  1579
fun-decl $in_array_full_extent_of 5 1
boehmes@33419
  1580
    type-con $ptr 0
boehmes@33419
  1581
    type-con $ptr 0
boehmes@33419
  1582
    type-con $ctype 0
boehmes@33419
  1583
    int
boehmes@33419
  1584
    bool
boehmes@33419
  1585
  attribute inline 1
boehmes@33419
  1586
    expr-attr
boehmes@33419
  1587
      true
boehmes@33419
  1588
fun-decl $in_array_extent_of 6 1
boehmes@33419
  1589
    type-con $state 0
boehmes@33419
  1590
    type-con $ptr 0
boehmes@33419
  1591
    type-con $ptr 0
boehmes@33419
  1592
    type-con $ctype 0
boehmes@33419
  1593
    int
boehmes@33419
  1594
    bool
boehmes@33419
  1595
  attribute inline 1
boehmes@33419
  1596
    expr-attr
boehmes@33419
  1597
      true
boehmes@33419
  1598
fun-decl $in_range 4 1
boehmes@33419
  1599
    int
boehmes@33419
  1600
    int
boehmes@33419
  1601
    int
boehmes@33419
  1602
    bool
boehmes@33419
  1603
  attribute inline 1
boehmes@33419
  1604
    expr-attr
boehmes@33419
  1605
      true
boehmes@33419
  1606
fun-decl $bool_to_int 2 1
boehmes@33419
  1607
    bool
boehmes@33419
  1608
    int
boehmes@33419
  1609
  attribute inline 1
boehmes@33419
  1610
    expr-attr
boehmes@33419
  1611
      true
boehmes@33419
  1612
fun-decl $int_to_bool 2 1
boehmes@33419
  1613
    int
boehmes@33419
  1614
    bool
boehmes@33419
  1615
  attribute inline 1
boehmes@33419
  1616
    expr-attr
boehmes@33419
  1617
      true
boehmes@33419
  1618
fun-decl $read_bool 3 1
boehmes@33419
  1619
    type-con $state 0
boehmes@33419
  1620
    type-con $ptr 0
boehmes@33419
  1621
    bool
boehmes@33419
  1622
  attribute inline 1
boehmes@33419
  1623
    expr-attr
boehmes@33419
  1624
      true
boehmes@33419
  1625
fun-decl $ite.int 4 3
boehmes@33419
  1626
    bool
boehmes@33419
  1627
    int
boehmes@33419
  1628
    int
boehmes@33419
  1629
    int
boehmes@33419
  1630
  attribute external 1
boehmes@33419
  1631
    string-attr ITE
boehmes@33419
  1632
  attribute bvz 1
boehmes@33419
  1633
    string-attr ITE
boehmes@33419
  1634
  attribute bvint 1
boehmes@33419
  1635
    string-attr ITE
boehmes@33419
  1636
fun-decl $ite.bool 4 3
boehmes@33419
  1637
    bool
boehmes@33419
  1638
    bool
boehmes@33419
  1639
    bool
boehmes@33419
  1640
    bool
boehmes@33419
  1641
  attribute external 1
boehmes@33419
  1642
    string-attr ITE
boehmes@33419
  1643
  attribute bvz 1
boehmes@33419
  1644
    string-attr ITE
boehmes@33419
  1645
  attribute bvint 1
boehmes@33419
  1646
    string-attr ITE
boehmes@33419
  1647
fun-decl $ite.ptr 4 3
boehmes@33419
  1648
    bool
boehmes@33419
  1649
    type-con $ptr 0
boehmes@33419
  1650
    type-con $ptr 0
boehmes@33419
  1651
    type-con $ptr 0
boehmes@33419
  1652
  attribute external 1
boehmes@33419
  1653
    string-attr ITE
boehmes@33419
  1654
  attribute bvz 1
boehmes@33419
  1655
    string-attr ITE
boehmes@33419
  1656
  attribute bvint 1
boehmes@33419
  1657
    string-attr ITE
boehmes@33419
  1658
fun-decl $ite.struct 4 3
boehmes@33419
  1659
    bool
boehmes@33419
  1660
    type-con $struct 0
boehmes@33419
  1661
    type-con $struct 0
boehmes@33419
  1662
    type-con $struct 0
boehmes@33419
  1663
  attribute external 1
boehmes@33419
  1664
    string-attr ITE
boehmes@33419
  1665
  attribute bvz 1
boehmes@33419
  1666
    string-attr ITE
boehmes@33419
  1667
  attribute bvint 1
boehmes@33419
  1668
    string-attr ITE
boehmes@33419
  1669
fun-decl $ite.ptrset 4 3
boehmes@33419
  1670
    bool
boehmes@33419
  1671
    type-con $ptrset 0
boehmes@33419
  1672
    type-con $ptrset 0
boehmes@33419
  1673
    type-con $ptrset 0
boehmes@33419
  1674
  attribute external 1
boehmes@33419
  1675
    string-attr ITE
boehmes@33419
  1676
  attribute bvz 1
boehmes@33419
  1677
    string-attr ITE
boehmes@33419
  1678
  attribute bvint 1
boehmes@33419
  1679
    string-attr ITE
boehmes@33419
  1680
fun-decl $ite.primitive 4 3
boehmes@33419
  1681
    bool
boehmes@33419
  1682
    type-con $primitive 0
boehmes@33419
  1683
    type-con $primitive 0
boehmes@33419
  1684
    type-con $primitive 0
boehmes@33419
  1685
  attribute external 1
boehmes@33419
  1686
    string-attr ITE
boehmes@33419
  1687
  attribute bvz 1
boehmes@33419
  1688
    string-attr ITE
boehmes@33419
  1689
  attribute bvint 1
boehmes@33419
  1690
    string-attr ITE
boehmes@33419
  1691
fun-decl $ite.record 4 3
boehmes@33419
  1692
    bool
boehmes@33419
  1693
    type-con $record 0
boehmes@33419
  1694
    type-con $record 0
boehmes@33419
  1695
    type-con $record 0
boehmes@33419
  1696
  attribute external 1
boehmes@33419
  1697
    string-attr ITE
boehmes@33419
  1698
  attribute bvz 1
boehmes@33419
  1699
    string-attr ITE
boehmes@33419
  1700
  attribute bvint 1
boehmes@33419
  1701
    string-attr ITE
boehmes@33419
  1702
fun-decl $bool_id 2 1
boehmes@33419
  1703
    bool
boehmes@33419
  1704
    bool
boehmes@33419
  1705
  attribute weight 1
boehmes@33419
  1706
    expr-attr
boehmes@33419
  1707
      int-num 0
boehmes@33419
  1708
fun-decl $min.i1 1 0
boehmes@33419
  1709
    int
boehmes@33419
  1710
fun-decl $max.i1 1 0
boehmes@33419
  1711
    int
boehmes@33419
  1712
fun-decl $min.i2 1 0
boehmes@33419
  1713
    int
boehmes@33419
  1714
fun-decl $max.i2 1 0
boehmes@33419
  1715
    int
boehmes@33419
  1716
fun-decl $min.i4 1 0
boehmes@33419
  1717
    int
boehmes@33419
  1718
fun-decl $max.i4 1 0
boehmes@33419
  1719
    int
boehmes@33419
  1720
fun-decl $min.i8 1 0
boehmes@33419
  1721
    int
boehmes@33419
  1722
fun-decl $max.i8 1 0
boehmes@33419
  1723
    int
boehmes@33419
  1724
fun-decl $max.u1 1 0
boehmes@33419
  1725
    int
boehmes@33419
  1726
fun-decl $max.u2 1 0
boehmes@33419
  1727
    int
boehmes@33419
  1728
fun-decl $max.u4 1 0
boehmes@33419
  1729
    int
boehmes@33419
  1730
fun-decl $max.u8 1 0
boehmes@33419
  1731
    int
boehmes@33419
  1732
fun-decl $in_range_i1 2 1
boehmes@33419
  1733
    int
boehmes@33419
  1734
    bool
boehmes@33419
  1735
  attribute inline 1
boehmes@33419
  1736
    expr-attr
boehmes@33419
  1737
      true
boehmes@33419
  1738
fun-decl $in_range_i2 2 1
boehmes@33419
  1739
    int
boehmes@33419
  1740
    bool
boehmes@33419
  1741
  attribute inline 1
boehmes@33419
  1742
    expr-attr
boehmes@33419
  1743
      true
boehmes@33419
  1744
fun-decl $in_range_i4 2 1
boehmes@33419
  1745
    int
boehmes@33419
  1746
    bool
boehmes@33419
  1747
  attribute inline 1
boehmes@33419
  1748
    expr-attr
boehmes@33419
  1749
      true
boehmes@33419
  1750
fun-decl $in_range_i8 2 1
boehmes@33419
  1751
    int
boehmes@33419
  1752
    bool
boehmes@33419
  1753
  attribute inline 1
boehmes@33419
  1754
    expr-attr
boehmes@33419
  1755
      true
boehmes@33419
  1756
fun-decl $in_range_u1 2 1
boehmes@33419
  1757
    int
boehmes@33419
  1758
    bool
boehmes@33419
  1759
  attribute inline 1
boehmes@33419
  1760
    expr-attr
boehmes@33419
  1761
      true
boehmes@33419
  1762
fun-decl $in_range_u2 2 1
boehmes@33419
  1763
    int
boehmes@33419
  1764
    bool
boehmes@33419
  1765
  attribute inline 1
boehmes@33419
  1766
    expr-attr
boehmes@33419
  1767
      true
boehmes@33419
  1768
fun-decl $in_range_u4 2 1
boehmes@33419
  1769
    int
boehmes@33419
  1770
    bool
boehmes@33419
  1771
  attribute inline 1
boehmes@33419
  1772
    expr-attr
boehmes@33419
  1773
      true
boehmes@33419
  1774
fun-decl $in_range_u8 2 1
boehmes@33419
  1775
    int
boehmes@33419
  1776
    bool
boehmes@33419
  1777
  attribute inline 1
boehmes@33419
  1778
    expr-attr
boehmes@33419
  1779
      true
boehmes@33419
  1780
fun-decl $in_range_div_i1 3 1
boehmes@33419
  1781
    int
boehmes@33419
  1782
    int
boehmes@33419
  1783
    bool
boehmes@33419
  1784
  attribute inline 1
boehmes@33419
  1785
    expr-attr
boehmes@33419
  1786
      true
boehmes@33419
  1787
fun-decl $in_range_div_i2 3 1
boehmes@33419
  1788
    int
boehmes@33419
  1789
    int
boehmes@33419
  1790
    bool
boehmes@33419
  1791
  attribute inline 1
boehmes@33419
  1792
    expr-attr
boehmes@33419
  1793
      true
boehmes@33419
  1794
fun-decl $in_range_div_i4 3 1
boehmes@33419
  1795
    int
boehmes@33419
  1796
    int
boehmes@33419
  1797
    bool
boehmes@33419
  1798
  attribute inline 1
boehmes@33419
  1799
    expr-attr
boehmes@33419
  1800
      true
boehmes@33419
  1801
fun-decl $in_range_div_i8 3 1
boehmes@33419
  1802
    int
boehmes@33419
  1803
    int
boehmes@33419
  1804
    bool
boehmes@33419
  1805
  attribute inline 1
boehmes@33419
  1806
    expr-attr
boehmes@33419
  1807
      true
boehmes@33419
  1808
fun-decl $read_i1 3 1
boehmes@33419
  1809
    type-con $state 0
boehmes@33419
  1810
    type-con $ptr 0
boehmes@33419
  1811
    int
boehmes@33419
  1812
  attribute weight 1
boehmes@33419
  1813
    expr-attr
boehmes@33419
  1814
      int-num 0
boehmes@33419
  1815
fun-decl $read_i2 3 1
boehmes@33419
  1816
    type-con $state 0
boehmes@33419
  1817
    type-con $ptr 0
boehmes@33419
  1818
    int
boehmes@33419
  1819
  attribute weight 1
boehmes@33419
  1820
    expr-attr
boehmes@33419
  1821
      int-num 0
boehmes@33419
  1822
fun-decl $read_i4 3 1
boehmes@33419
  1823
    type-con $state 0
boehmes@33419
  1824
    type-con $ptr 0
boehmes@33419
  1825
    int
boehmes@33419
  1826
  attribute weight 1
boehmes@33419
  1827
    expr-attr
boehmes@33419
  1828
      int-num 0
boehmes@33419
  1829
fun-decl $read_i8 3 1
boehmes@33419
  1830
    type-con $state 0
boehmes@33419
  1831
    type-con $ptr 0
boehmes@33419
  1832
    int
boehmes@33419
  1833
  attribute weight 1
boehmes@33419
  1834
    expr-attr
boehmes@33419
  1835
      int-num 0
boehmes@33419
  1836
fun-decl $read_u1 3 1
boehmes@33419
  1837
    type-con $state 0
boehmes@33419
  1838
    type-con $ptr 0
boehmes@33419
  1839
    int
boehmes@33419
  1840
  attribute weight 1
boehmes@33419
  1841
    expr-attr
boehmes@33419
  1842
      int-num 0
boehmes@33419
  1843
fun-decl $read_u2 3 1
boehmes@33419
  1844
    type-con $state 0
boehmes@33419
  1845
    type-con $ptr 0
boehmes@33419
  1846
    int
boehmes@33419
  1847
  attribute weight 1
boehmes@33419
  1848
    expr-attr
boehmes@33419
  1849
      int-num 0
boehmes@33419
  1850
fun-decl $read_u4 3 1
boehmes@33419
  1851
    type-con $state 0
boehmes@33419
  1852
    type-con $ptr 0
boehmes@33419
  1853
    int
boehmes@33419
  1854
  attribute weight 1
boehmes@33419
  1855
    expr-attr
boehmes@33419
  1856
      int-num 0
boehmes@33419
  1857
fun-decl $read_u8 3 1
boehmes@33419
  1858
    type-con $state 0
boehmes@33419
  1859
    type-con $ptr 0
boehmes@33419
  1860
    int
boehmes@33419
  1861
  attribute weight 1
boehmes@33419
  1862
    expr-attr
boehmes@33419
  1863
      int-num 0
boehmes@33419
  1864
fun-decl $ptr_to_u8 2 0
boehmes@33419
  1865
    type-con $ptr 0
boehmes@33419
  1866
    int
boehmes@33419
  1867
fun-decl $ptr_to_i8 2 0
boehmes@33419
  1868
    type-con $ptr 0
boehmes@33419
  1869
    int
boehmes@33419
  1870
fun-decl $ptr_to_u4 2 0
boehmes@33419
  1871
    type-con $ptr 0
boehmes@33419
  1872
    int
boehmes@33419
  1873
fun-decl $ptr_to_i4 2 0
boehmes@33419
  1874
    type-con $ptr 0
boehmes@33419
  1875
    int
boehmes@33419
  1876
fun-decl $u8_to_ptr 2 1
boehmes@33419
  1877
    int
boehmes@33419
  1878
    type-con $ptr 0
boehmes@33419
  1879
  attribute inline 1
boehmes@33419
  1880
    expr-attr
boehmes@33419
  1881
      true
boehmes@33419
  1882
fun-decl $i8_to_ptr 2 1
boehmes@33419
  1883
    int
boehmes@33419
  1884
    type-con $ptr 0
boehmes@33419
  1885
  attribute inline 1
boehmes@33419
  1886
    expr-attr
boehmes@33419
  1887
      true
boehmes@33419
  1888
fun-decl $u4_to_ptr 2 1
boehmes@33419
  1889
    int
boehmes@33419
  1890
    type-con $ptr 0
boehmes@33419
  1891
  attribute inline 1
boehmes@33419
  1892
    expr-attr
boehmes@33419
  1893
      true
boehmes@33419
  1894
fun-decl $i4_to_ptr 2 1
boehmes@33419
  1895
    int
boehmes@33419
  1896
    type-con $ptr 0
boehmes@33419
  1897
  attribute inline 1
boehmes@33419
  1898
    expr-attr
boehmes@33419
  1899
      true
boehmes@33419
  1900
fun-decl $byte_ptr_subtraction 3 1
boehmes@33419
  1901
    type-con $ptr 0
boehmes@33419
  1902
    type-con $ptr 0
boehmes@33419
  1903
    int
boehmes@33419
  1904
  attribute weight 1
boehmes@33419
  1905
    expr-attr
boehmes@33419
  1906
      int-num 0
boehmes@33419
  1907
fun-decl $_pow2 2 0
boehmes@33419
  1908
    int
boehmes@33419
  1909
    int
boehmes@33419
  1910
fun-decl $_or 4 0
boehmes@33419
  1911
    type-con $ctype 0
boehmes@33419
  1912
    int
boehmes@33419
  1913
    int
boehmes@33419
  1914
    int
boehmes@33419
  1915
fun-decl $_xor 4 0
boehmes@33419
  1916
    type-con $ctype 0
boehmes@33419
  1917
    int
boehmes@33419
  1918
    int
boehmes@33419
  1919
    int
boehmes@33419
  1920
fun-decl $_and 4 0
boehmes@33419
  1921
    type-con $ctype 0
boehmes@33419
  1922
    int
boehmes@33419
  1923
    int
boehmes@33419
  1924
    int
boehmes@33419
  1925
fun-decl $_not 3 0
boehmes@33419
  1926
    type-con $ctype 0
boehmes@33419
  1927
    int
boehmes@33419
  1928
    int
boehmes@33419
  1929
fun-decl $unchk_add 4 1
boehmes@33419
  1930
    type-con $ctype 0
boehmes@33419
  1931
    int
boehmes@33419
  1932
    int
boehmes@33419
  1933
    int
boehmes@33419
  1934
  attribute weight 1
boehmes@33419
  1935
    expr-attr
boehmes@33419
  1936
      int-num 0
boehmes@33419
  1937
fun-decl $unchk_sub 4 1
boehmes@33419
  1938
    type-con $ctype 0
boehmes@33419
  1939
    int
boehmes@33419
  1940
    int
boehmes@33419
  1941
    int
boehmes@33419
  1942
  attribute weight 1
boehmes@33419
  1943
    expr-attr
boehmes@33419
  1944
      int-num 0
boehmes@33419
  1945
fun-decl $unchk_mul 4 1
boehmes@33419
  1946
    type-con $ctype 0
boehmes@33419
  1947
    int
boehmes@33419
  1948
    int
boehmes@33419
  1949
    int
boehmes@33419
  1950
  attribute weight 1
boehmes@33419
  1951
    expr-attr
boehmes@33419
  1952
      int-num 0
boehmes@33419
  1953
fun-decl $unchk_div 4 1
boehmes@33419
  1954
    type-con $ctype 0
boehmes@33419
  1955
    int
boehmes@33419
  1956
    int
boehmes@33419
  1957
    int
boehmes@33419
  1958
  attribute weight 1
boehmes@33419
  1959
    expr-attr
boehmes@33419
  1960
      int-num 0
boehmes@33419
  1961
fun-decl $unchk_mod 4 1
boehmes@33419
  1962
    type-con $ctype 0
boehmes@33419
  1963
    int
boehmes@33419
  1964
    int
boehmes@33419
  1965
    int
boehmes@33419
  1966
  attribute weight 1
boehmes@33419
  1967
    expr-attr
boehmes@33419
  1968
      int-num 0
boehmes@33419
  1969
fun-decl $_shl 4 1
boehmes@33419
  1970
    type-con $ctype 0
boehmes@33419
  1971
    int
boehmes@33419
  1972
    int
boehmes@33419
  1973
    int
boehmes@33419
  1974
  attribute weight 1
boehmes@33419
  1975
    expr-attr
boehmes@33419
  1976
      int-num 0
boehmes@33419
  1977
fun-decl $_shr 3 1
boehmes@33419
  1978
    int
boehmes@33419
  1979
    int
boehmes@33419
  1980
    int
boehmes@33419
  1981
  attribute weight 1
boehmes@33419
  1982
    expr-attr
boehmes@33419
  1983
      int-num 0
boehmes@33419
  1984
fun-decl $bv_extract_signed 5 0
boehmes@33419
  1985
    int
boehmes@33419
  1986
    int
boehmes@33419
  1987
    int
boehmes@33419
  1988
    int
boehmes@33419
  1989
    int
boehmes@33419
  1990
fun-decl $bv_extract_unsigned 5 0
boehmes@33419
  1991
    int
boehmes@33419
  1992
    int
boehmes@33419
  1993
    int
boehmes@33419
  1994
    int
boehmes@33419
  1995
    int
boehmes@33419
  1996
fun-decl $bv_update 6 0
boehmes@33419
  1997
    int
boehmes@33419
  1998
    int
boehmes@33419
  1999
    int
boehmes@33419
  2000
    int
boehmes@33419
  2001
    int
boehmes@33419
  2002
    int
boehmes@33419
  2003
fun-decl $unchecked 3 0
boehmes@33419
  2004
    type-con $ctype 0
boehmes@33419
  2005
    int
boehmes@33419
  2006
    int
boehmes@33419
  2007
fun-decl $in_range_t 3 0
boehmes@33419
  2008
    type-con $ctype 0
boehmes@33419
  2009
    int
boehmes@33419
  2010
    bool
boehmes@33419
  2011
fun-decl $_mul 3 1
boehmes@33419
  2012
    int
boehmes@33419
  2013
    int
boehmes@33419
  2014
    int
boehmes@33419
  2015
  attribute weight 1
boehmes@33419
  2016
    expr-attr
boehmes@33419
  2017
      int-num 0
boehmes@33419
  2018
fun-decl $get_string_literal 3 0
boehmes@33419
  2019
    int
boehmes@33419
  2020
    int
boehmes@33419
  2021
    type-con $ptr 0
boehmes@33419
  2022
fun-decl $get_fnptr 3 0
boehmes@33419
  2023
    int
boehmes@33419
  2024
    type-con $ctype 0
boehmes@33419
  2025
    type-con $ptr 0
boehmes@33419
  2026
fun-decl $get_fnptr_ref 2 0
boehmes@33419
  2027
    int
boehmes@33419
  2028
    int
boehmes@33419
  2029
fun-decl $get_fnptr_inv 2 0
boehmes@33419
  2030
    int
boehmes@33419
  2031
    int
boehmes@33419
  2032
fun-decl $is_fnptr_type 2 0
boehmes@33419
  2033
    type-con $ctype 0
boehmes@33419
  2034
    bool
boehmes@33419
  2035
fun-decl $is_math_type 2 0
boehmes@33419
  2036
    type-con $ctype 0
boehmes@33419
  2037
    bool
boehmes@33419
  2038
fun-decl $claims_obj 3 0
boehmes@33419
  2039
    type-con $ptr 0
boehmes@33419
  2040
    type-con $ptr 0
boehmes@33419
  2041
    bool
boehmes@33419
  2042
fun-decl $valid_claim 3 0
boehmes@33419
  2043
    type-con $state 0
boehmes@33419
  2044
    type-con $ptr 0
boehmes@33419
  2045
    bool
boehmes@33419
  2046
fun-decl $claim_initial_assumptions 4 1
boehmes@33419
  2047
    type-con $state 0
boehmes@33419
  2048
    type-con $ptr 0
boehmes@33419
  2049
    type-con $token 0
boehmes@33419
  2050
    bool
boehmes@33419
  2051
  attribute inline 1
boehmes@33419
  2052
    expr-attr
boehmes@33419
  2053
      true
boehmes@33419
  2054
fun-decl $claim_transitivity_assumptions 5 1
boehmes@33419
  2055
    type-con $state 0
boehmes@33419
  2056
    type-con $state 0
boehmes@33419
  2057
    type-con $ptr 0
boehmes@33419
  2058
    type-con $token 0
boehmes@33419
  2059
    bool
boehmes@33419
  2060
  attribute inline 1
boehmes@33419
  2061
    expr-attr
boehmes@33419
  2062
      true
boehmes@33419
  2063
fun-decl $valid_claim_impl 3 1
boehmes@33419
  2064
    type-con $state 0
boehmes@33419
  2065
    type-con $state 0
boehmes@33419
  2066
    bool
boehmes@33419
  2067
  attribute inline 1
boehmes@33419
  2068
    expr-attr
boehmes@33419
  2069
      true
boehmes@33419
  2070
fun-decl $claims_claim 3 0
boehmes@33419
  2071
    type-con $ptr 0
boehmes@33419
  2072
    type-con $ptr 0
boehmes@33419
  2073
    bool
boehmes@33419
  2074
fun-decl $not_shared 3 1
boehmes@33419
  2075
    type-con $state 0
boehmes@33419
  2076
    type-con $ptr 0
boehmes@33419
  2077
    bool
boehmes@33419
  2078
  attribute weight 1
boehmes@33419
  2079
    expr-attr
boehmes@33419
  2080
      int-num 0
boehmes@33419
  2081
fun-decl $claimed_closed 3 1
boehmes@33419
  2082
    type-con $state 0
boehmes@33419
  2083
    type-con $ptr 0
boehmes@33419
  2084
    bool
boehmes@33419
  2085
  attribute weight 1
boehmes@33419
  2086
    expr-attr
boehmes@33419
  2087
      int-num 0
boehmes@33419
  2088
fun-decl $no_claim 1 1
boehmes@33419
  2089
    type-con $ptr 0
boehmes@33419
  2090
  attribute unique 0
boehmes@33419
  2091
fun-decl $ref_cnt 3 1
boehmes@33419
  2092
    type-con $state 0
boehmes@33419
  2093
    type-con $ptr 0
boehmes@33419
  2094
    int
boehmes@33419
  2095
  attribute weight 1
boehmes@33419
  2096
    expr-attr
boehmes@33419
  2097
      int-num 0
boehmes@33419
  2098
fun-decl $is_claimable 2 0
boehmes@33419
  2099
    type-con $ctype 0
boehmes@33419
  2100
    bool
boehmes@33419
  2101
fun-decl $is_thread_local_storage 2 0
boehmes@33419
  2102
    type-con $ctype 0
boehmes@33419
  2103
    bool
boehmes@33419
  2104
fun-decl $frame_level 2 0
boehmes@33419
  2105
    type-con $pure_function 0
boehmes@33419
  2106
    int
boehmes@33419
  2107
fun-decl $current_frame_level 1 0
boehmes@33419
  2108
    int
boehmes@33419
  2109
fun-decl $can_use_all_frame_axioms 2 1
boehmes@33419
  2110
    type-con $state 0
boehmes@33419
  2111
    bool
boehmes@33419
  2112
  attribute inline 1
boehmes@33419
  2113
    expr-attr
boehmes@33419
  2114
      true
boehmes@33419
  2115
fun-decl $can_use_frame_axiom_of 2 1
boehmes@33419
  2116
    type-con $pure_function 0
boehmes@33419
  2117
    bool
boehmes@33419
  2118
  attribute inline 1
boehmes@33419
  2119
    expr-attr
boehmes@33419
  2120
      true
boehmes@33419
  2121
fun-decl $reads_check_pre 2 0
boehmes@33419
  2122
    type-con $state 0
boehmes@33419
  2123
    bool
boehmes@33419
  2124
fun-decl $reads_check_post 2 0
boehmes@33419
  2125
    type-con $state 0
boehmes@33419
  2126
    bool
boehmes@33419
  2127
fun-decl $start_here 1 0
boehmes@33419
  2128
    bool
boehmes@33419
  2129
fun-decl $ptrset_to_int 2 0
boehmes@33419
  2130
    type-con $ptrset 0
boehmes@33419
  2131
    int
boehmes@33419
  2132
fun-decl $int_to_ptrset 2 0
boehmes@33419
  2133
    int
boehmes@33419
  2134
    type-con $ptrset 0
boehmes@33419
  2135
fun-decl $version_to_int 2 0
boehmes@33419
  2136
    type-con $version 0
boehmes@33419
  2137
    int
boehmes@33419
  2138
fun-decl $int_to_version 2 0
boehmes@33419
  2139
    int
boehmes@33419
  2140
    type-con $version 0
boehmes@33419
  2141
fun-decl $vol_version_to_int 2 0
boehmes@33419
  2142
    type-con $vol_version 0
boehmes@33419
  2143
    int
boehmes@33419
  2144
fun-decl $int_to_vol_version 2 0
boehmes@33419
  2145
    int
boehmes@33419
  2146
    type-con $vol_version 0
boehmes@33419
  2147
fun-decl $ptr_to_int 2 0
boehmes@33419
  2148
    type-con $ptr 0
boehmes@33419
  2149
    int
boehmes@33419
  2150
fun-decl $int_to_ptr 2 0
boehmes@33419
  2151
    int
boehmes@33419
  2152
    type-con $ptr 0
boehmes@33419
  2153
fun-decl $precise_test 2 0
boehmes@33419
  2154
    type-con $ptr 0
boehmes@33419
  2155
    bool
boehmes@33419
  2156
fun-decl $updated_only_values 4 0
boehmes@33419
  2157
    type-con $state 0
boehmes@33419
  2158
    type-con $state 0
boehmes@33419
  2159
    type-con $ptrset 0
boehmes@33419
  2160
    bool
boehmes@33419
  2161
fun-decl $updated_only_domains 4 0
boehmes@33419
  2162
    type-con $state 0
boehmes@33419
  2163
    type-con $state 0
boehmes@33419
  2164
    type-con $ptrset 0
boehmes@33419
  2165
    bool
boehmes@33419
  2166
fun-decl $domain_updated_at 5 0
boehmes@33419
  2167
    type-con $state 0
boehmes@33419
  2168
    type-con $state 0
boehmes@33419
  2169
    type-con $ptr 0
boehmes@33419
  2170
    type-con $ptrset 0
boehmes@33419
  2171
    bool
boehmes@33419
  2172
fun-decl l#public 1 1
boehmes@33419
  2173
    type-con $label 0
boehmes@33419
  2174
  attribute unique 0
boehmes@33419
  2175
fun-decl #tok$1^16.24 1 1
boehmes@33419
  2176
    type-con $token 0
boehmes@33419
  2177
  attribute unique 0
boehmes@33419
  2178
fun-decl #tok$1^24.47 1 1
boehmes@33419
  2179
    type-con $token 0
boehmes@33419
  2180
  attribute unique 0
boehmes@33419
  2181
fun-decl #tok$1^23.7 1 1
boehmes@33419
  2182
    type-con $token 0
boehmes@33419
  2183
  attribute unique 0
boehmes@33419
  2184
fun-decl #tok$1^16.3 1 1
boehmes@33419
  2185
    type-con $token 0
boehmes@33419
  2186
  attribute unique 0
boehmes@33419
  2187
fun-decl #loc.p 1 1
boehmes@33419
  2188
    type-con $token 0
boehmes@33419
  2189
  attribute unique 0
boehmes@33419
  2190
fun-decl #tok$1^16.8 1 1
boehmes@33419
  2191
    type-con $token 0
boehmes@33419
  2192
  attribute unique 0
boehmes@33419
  2193
fun-decl #loc.witness 1 1
boehmes@33419
  2194
    type-con $token 0
boehmes@33419
  2195
  attribute unique 0
boehmes@33419
  2196
fun-decl #tok$1^14.3 1 1
boehmes@33419
  2197
    type-con $token 0
boehmes@33419
  2198
  attribute unique 0
boehmes@33419
  2199
fun-decl #loc.max 1 1
boehmes@33419
  2200
    type-con $token 0
boehmes@33419
  2201
  attribute unique 0
boehmes@33419
  2202
fun-decl #tok$1^12.3 1 1
boehmes@33419
  2203
    type-con $token 0
boehmes@33419
  2204
  attribute unique 0
boehmes@33419
  2205
fun-decl #loc.len 1 1
boehmes@33419
  2206
    type-con $token 0
boehmes@33419
  2207
  attribute unique 0
boehmes@33419
  2208
fun-decl #distTp1 1 1
boehmes@33419
  2209
    type-con $ctype 0
boehmes@33419
  2210
  attribute unique 0
boehmes@33419
  2211
fun-decl #loc.arr 1 1
boehmes@33419
  2212
    type-con $token 0
boehmes@33419
  2213
  attribute unique 0
boehmes@33419
  2214
fun-decl #tok$1^6.1 1 1
boehmes@33419
  2215
    type-con $token 0
boehmes@33419
  2216
  attribute unique 0
boehmes@33419
  2217
fun-decl #file^Z?3A?5CC?5Cmax.c 1 1
boehmes@33419
  2218
    type-con $token 0
boehmes@33419
  2219
  attribute unique 0
boehmes@33419
  2220
axiom 0
boehmes@33419
  2221
    =
boehmes@33419
  2222
    fun $sizeof 1
boehmes@33419
  2223
    fun ^^i1 0
boehmes@33419
  2224
    int-num 1
boehmes@33419
  2225
axiom 0
boehmes@33419
  2226
    =
boehmes@33419
  2227
    fun $sizeof 1
boehmes@33419
  2228
    fun ^^i2 0
boehmes@33419
  2229
    int-num 2
boehmes@33419
  2230
axiom 0
boehmes@33419
  2231
    =
boehmes@33419
  2232
    fun $sizeof 1
boehmes@33419
  2233
    fun ^^i4 0
boehmes@33419
  2234
    int-num 4
boehmes@33419
  2235
axiom 0
boehmes@33419
  2236
    =
boehmes@33419
  2237
    fun $sizeof 1
boehmes@33419
  2238
    fun ^^i8 0
boehmes@33419
  2239
    int-num 8
boehmes@33419
  2240
axiom 0
boehmes@33419
  2241
    =
boehmes@33419
  2242
    fun $sizeof 1
boehmes@33419
  2243
    fun ^^u1 0
boehmes@33419
  2244
    int-num 1
boehmes@33419
  2245
axiom 0
boehmes@33419
  2246
    =
boehmes@33419
  2247
    fun $sizeof 1
boehmes@33419
  2248
    fun ^^u2 0
boehmes@33419
  2249
    int-num 2
boehmes@33419
  2250
axiom 0
boehmes@33419
  2251
    =
boehmes@33419
  2252
    fun $sizeof 1
boehmes@33419
  2253
    fun ^^u4 0
boehmes@33419
  2254
    int-num 4
boehmes@33419
  2255
axiom 0
boehmes@33419
  2256
    =
boehmes@33419
  2257
    fun $sizeof 1
boehmes@33419
  2258
    fun ^^u8 0
boehmes@33419
  2259
    int-num 8
boehmes@33419
  2260
axiom 0
boehmes@33419
  2261
    =
boehmes@33419
  2262
    fun $sizeof 1
boehmes@33419
  2263
    fun ^^f4 0
boehmes@33419
  2264
    int-num 4
boehmes@33419
  2265
axiom 0
boehmes@33419
  2266
    =
boehmes@33419
  2267
    fun $sizeof 1
boehmes@33419
  2268
    fun ^^f8 0
boehmes@33419
  2269
    int-num 8
boehmes@33419
  2270
axiom 0
boehmes@33419
  2271
    =
boehmes@33419
  2272
    fun $sizeof 1
boehmes@33419
  2273
    fun ^$#thread_id_t 0
boehmes@33419
  2274
    int-num 1
boehmes@33419
  2275
axiom 0
boehmes@33419
  2276
    =
boehmes@33419
  2277
    fun $sizeof 1
boehmes@33419
  2278
    fun ^$#ptrset 0
boehmes@33419
  2279
    int-num 1
boehmes@33419
  2280
axiom 0
boehmes@33419
  2281
    =
boehmes@33419
  2282
    fun $ptr_level 1
boehmes@33419
  2283
    fun ^^i1 0
boehmes@33419
  2284
    int-num 0
boehmes@33419
  2285
axiom 0
boehmes@33419
  2286
    =
boehmes@33419
  2287
    fun $ptr_level 1
boehmes@33419
  2288
    fun ^^i2 0
boehmes@33419
  2289
    int-num 0
boehmes@33419
  2290
axiom 0
boehmes@33419
  2291
    =
boehmes@33419
  2292
    fun $ptr_level 1
boehmes@33419
  2293
    fun ^^i4 0
boehmes@33419
  2294
    int-num 0
boehmes@33419
  2295
axiom 0
boehmes@33419
  2296
    =
boehmes@33419
  2297
    fun $ptr_level 1
boehmes@33419
  2298
    fun ^^i8 0
boehmes@33419
  2299
    int-num 0
boehmes@33419
  2300
axiom 0
boehmes@33419
  2301
    =
boehmes@33419
  2302
    fun $ptr_level 1
boehmes@33419
  2303
    fun ^^u1 0
boehmes@33419
  2304
    int-num 0
boehmes@33419
  2305
axiom 0
boehmes@33419
  2306
    =
boehmes@33419
  2307
    fun $ptr_level 1
boehmes@33419
  2308
    fun ^^u2 0
boehmes@33419
  2309
    int-num 0
boehmes@33419
  2310
axiom 0
boehmes@33419
  2311
    =
boehmes@33419
  2312
    fun $ptr_level 1
boehmes@33419
  2313
    fun ^^u4 0
boehmes@33419
  2314
    int-num 0
boehmes@33419
  2315
axiom 0
boehmes@33419
  2316
    =
boehmes@33419
  2317
    fun $ptr_level 1
boehmes@33419
  2318
    fun ^^u8 0
boehmes@33419
  2319
    int-num 0
boehmes@33419
  2320
axiom 0
boehmes@33419
  2321
    =
boehmes@33419
  2322
    fun $ptr_level 1
boehmes@33419
  2323
    fun ^^f4 0
boehmes@33419
  2324
    int-num 0
boehmes@33419
  2325
axiom 0
boehmes@33419
  2326
    =
boehmes@33419
  2327
    fun $ptr_level 1
boehmes@33419
  2328
    fun ^^f8 0
boehmes@33419
  2329
    int-num 0
boehmes@33419
  2330
axiom 0
boehmes@33419
  2331
    =
boehmes@33419
  2332
    fun $ptr_level 1
boehmes@33419
  2333
    fun ^^mathint 0
boehmes@33419
  2334
    int-num 0
boehmes@33419
  2335
axiom 0
boehmes@33419
  2336
    =
boehmes@33419
  2337
    fun $ptr_level 1
boehmes@33419
  2338
    fun ^^bool 0
boehmes@33419
  2339
    int-num 0
boehmes@33419
  2340
axiom 0
boehmes@33419
  2341
    =
boehmes@33419
  2342
    fun $ptr_level 1
boehmes@33419
  2343
    fun ^^void 0
boehmes@33419
  2344
    int-num 0
boehmes@33419
  2345
axiom 0
boehmes@33419
  2346
    =
boehmes@33419
  2347
    fun $ptr_level 1
boehmes@33419
  2348
    fun ^^claim 0
boehmes@33419
  2349
    int-num 0
boehmes@33419
  2350
axiom 0
boehmes@33419
  2351
    =
boehmes@33419
  2352
    fun $ptr_level 1
boehmes@33419
  2353
    fun ^^root_emb 0
boehmes@33419
  2354
    int-num 0
boehmes@33419
  2355
axiom 0
boehmes@33419
  2356
    =
boehmes@33419
  2357
    fun $ptr_level 1
boehmes@33419
  2358
    fun ^$#ptrset 0
boehmes@33419
  2359
    int-num 0
boehmes@33419
  2360
axiom 0
boehmes@33419
  2361
    =
boehmes@33419
  2362
    fun $ptr_level 1
boehmes@33419
  2363
    fun ^$#thread_id_t 0
boehmes@33419
  2364
    int-num 0
boehmes@33419
  2365
axiom 0
boehmes@33419
  2366
    =
boehmes@33419
  2367
    fun $ptr_level 1
boehmes@33419
  2368
    fun ^$#state_t 0
boehmes@33419
  2369
    int-num 0
boehmes@33419
  2370
axiom 0
boehmes@33419
  2371
    =
boehmes@33419
  2372
    fun $ptr_level 1
boehmes@33419
  2373
    fun ^$#struct 0
boehmes@33419
  2374
    int-num 0
boehmes@33419
  2375
axiom 0
boehmes@33419
  2376
    fun $is_composite 1
boehmes@33419
  2377
    fun ^^claim 0
boehmes@33419
  2378
axiom 0
boehmes@33419
  2379
    fun $is_composite 1
boehmes@33419
  2380
    fun ^^root_emb 0
boehmes@33419
  2381
axiom 0
boehmes@33419
  2382
    forall 1 1 3
boehmes@33419
  2383
      var #n
boehmes@33419
  2384
        type-con $ctype 0
boehmes@33419
  2385
      pat 1
boehmes@33419
  2386
        fun $ptr_to 1
boehmes@33419
  2387
        var #n
boehmes@33419
  2388
          type-con $ctype 0
boehmes@33419
  2389
      attribute qid 1
boehmes@33419
  2390
        string-attr VccPrelu.145:15
boehmes@33419
  2391
      attribute uniqueId 1
boehmes@33419
  2392
        string-attr 4
boehmes@33419
  2393
      attribute bvZ3Native 1
boehmes@33419
  2394
        string-attr False
boehmes@33419
  2395
    =
boehmes@33419
  2396
    fun $unptr_to 1
boehmes@33419
  2397
    fun $ptr_to 1
boehmes@33419
  2398
    var #n
boehmes@33419
  2399
      type-con $ctype 0
boehmes@33419
  2400
    var #n
boehmes@33419
  2401
      type-con $ctype 0
boehmes@33419
  2402
axiom 0
boehmes@33419
  2403
    forall 1 1 3
boehmes@33419
  2404
      var #n
boehmes@33419
  2405
        type-con $ctype 0
boehmes@33419
  2406
      pat 1
boehmes@33419
  2407
        fun $ptr_to 1
boehmes@33419
  2408
        var #n
boehmes@33419
  2409
          type-con $ctype 0
boehmes@33419
  2410
      attribute qid 1
boehmes@33419
  2411
        string-attr VccPrelu.146:15
boehmes@33419
  2412
      attribute uniqueId 1
boehmes@33419
  2413
        string-attr 5
boehmes@33419
  2414
      attribute bvZ3Native 1
boehmes@33419
  2415
        string-attr False
boehmes@33419
  2416
    =
boehmes@33419
  2417
    fun $sizeof 1
boehmes@33419
  2418
    fun $ptr_to 1
boehmes@33419
  2419
    var #n
boehmes@33419
  2420
      type-con $ctype 0
boehmes@33419
  2421
    int-num 8
boehmes@33419
  2422
axiom 0
boehmes@33419
  2423
    forall 2 1 3
boehmes@33419
  2424
      var #r
boehmes@33419
  2425
        type-con $ctype 0
boehmes@33419
  2426
      var #d
boehmes@33419
  2427
        type-con $ctype 0
boehmes@33419
  2428
      pat 1
boehmes@33419
  2429
        fun $map_t 2
boehmes@33419
  2430
        var #r
boehmes@33419
  2431
          type-con $ctype 0
boehmes@33419
  2432
        var #d
boehmes@33419
  2433
          type-con $ctype 0
boehmes@33419
  2434
      attribute qid 1
boehmes@33419
  2435
        string-attr VccPrelu.152:15
boehmes@33419
  2436
      attribute uniqueId 1
boehmes@33419
  2437
        string-attr 6
boehmes@33419
  2438
      attribute bvZ3Native 1
boehmes@33419
  2439
        string-attr False
boehmes@33419
  2440
    =
boehmes@33419
  2441
    fun $map_domain 1
boehmes@33419
  2442
    fun $map_t 2
boehmes@33419
  2443
    var #r
boehmes@33419
  2444
      type-con $ctype 0
boehmes@33419
  2445
    var #d
boehmes@33419
  2446
      type-con $ctype 0
boehmes@33419
  2447
    var #d
boehmes@33419
  2448
      type-con $ctype 0
boehmes@33419
  2449
axiom 0
boehmes@33419
  2450
    forall 2 1 3
boehmes@33419
  2451
      var #r
boehmes@33419
  2452
        type-con $ctype 0
boehmes@33419
  2453
      var #d
boehmes@33419
  2454
        type-con $ctype 0
boehmes@33419
  2455
      pat 1
boehmes@33419
  2456
        fun $map_t 2
boehmes@33419
  2457
        var #r
boehmes@33419
  2458
          type-con $ctype 0
boehmes@33419
  2459
        var #d
boehmes@33419
  2460
          type-con $ctype 0
boehmes@33419
  2461
      attribute qid 1
boehmes@33419
  2462
        string-attr VccPrelu.153:15
boehmes@33419
  2463
      attribute uniqueId 1
boehmes@33419
  2464
        string-attr 7
boehmes@33419
  2465
      attribute bvZ3Native 1
boehmes@33419
  2466
        string-attr False
boehmes@33419
  2467
    =
boehmes@33419
  2468
    fun $map_range 1
boehmes@33419
  2469
    fun $map_t 2
boehmes@33419
  2470
    var #r
boehmes@33419
  2471
      type-con $ctype 0
boehmes@33419
  2472
    var #d
boehmes@33419
  2473
      type-con $ctype 0
boehmes@33419
  2474
    var #r
boehmes@33419
  2475
      type-con $ctype 0
boehmes@33419
  2476
axiom 0
boehmes@33419
  2477
    forall 1 1 3
boehmes@33419
  2478
      var #n
boehmes@33419
  2479
        type-con $ctype 0
boehmes@33419
  2480
      pat 1
boehmes@33419
  2481
        fun $ptr_to 1
boehmes@33419
  2482
        var #n
boehmes@33419
  2483
          type-con $ctype 0
boehmes@33419
  2484
      attribute qid 1
boehmes@33419
  2485
        string-attr VccPrelu.158:15
boehmes@33419
  2486
      attribute uniqueId 1
boehmes@33419
  2487
        string-attr 8
boehmes@33419
  2488
      attribute bvZ3Native 1
boehmes@33419
  2489
        string-attr False
boehmes@33419
  2490
    =
boehmes@33419
  2491
    fun $ptr_level 1
boehmes@33419
  2492
    fun $ptr_to 1
boehmes@33419
  2493
    var #n
boehmes@33419
  2494
      type-con $ctype 0
boehmes@33419
  2495
    +
boehmes@33419
  2496
    fun $ptr_level 1
boehmes@33419
  2497
    var #n
boehmes@33419
  2498
      type-con $ctype 0
boehmes@33419
  2499
    int-num 17
boehmes@33419
  2500
axiom 0
boehmes@33419
  2501
    forall 2 1 3
boehmes@33419
  2502
      var #r
boehmes@33419
  2503
        type-con $ctype 0
boehmes@33419
  2504
      var #d
boehmes@33419
  2505
        type-con $ctype 0
boehmes@33419
  2506
      pat 1
boehmes@33419
  2507
        fun $map_t 2
boehmes@33419
  2508
        var #r
boehmes@33419
  2509
          type-con $ctype 0
boehmes@33419
  2510
        var #d
boehmes@33419
  2511
          type-con $ctype 0
boehmes@33419
  2512
      attribute qid 1
boehmes@33419
  2513
        string-attr VccPrelu.159:15
boehmes@33419
  2514
      attribute uniqueId 1
boehmes@33419
  2515
        string-attr 9
boehmes@33419
  2516
      attribute bvZ3Native 1
boehmes@33419
  2517
        string-attr False
boehmes@33419
  2518
    =
boehmes@33419
  2519
    fun $ptr_level 1
boehmes@33419
  2520
    fun $map_t 2
boehmes@33419
  2521
    var #r
boehmes@33419
  2522
      type-con $ctype 0
boehmes@33419
  2523
    var #d
boehmes@33419
  2524
      type-con $ctype 0
boehmes@33419
  2525
    +
boehmes@33419
  2526
    fun $ptr_level 1
boehmes@33419
  2527
    var #r
boehmes@33419
  2528
      type-con $ctype 0
boehmes@33419
  2529
    int-num 23
boehmes@33419
  2530
axiom 0
boehmes@33419
  2531
    forall 1 1 4
boehmes@33419
  2532
      var t
boehmes@33419
  2533
        type-con $ctype 0
boehmes@33419
  2534
      pat 1
boehmes@33419
  2535
        fun $is_primitive 1
boehmes@33419
  2536
        var t
boehmes@33419
  2537
          type-con $ctype 0
boehmes@33419
  2538
      attribute qid 1
boehmes@33419
  2539
        string-attr VccPrelu.167:36
boehmes@33419
  2540
      attribute uniqueId 1
boehmes@33419
  2541
        string-attr 10
boehmes@33419
  2542
      attribute bvZ3Native 1
boehmes@33419
  2543
        string-attr False
boehmes@33419
  2544
      attribute weight 1
boehmes@33419
  2545
        expr-attr
boehmes@33419
  2546
          int-num 0
boehmes@33419
  2547
    =
boehmes@33419
  2548
    fun $is_primitive 1
boehmes@33419
  2549
    var t
boehmes@33419
  2550
      type-con $ctype 0
boehmes@33419
  2551
    =
boehmes@33419
  2552
    fun $kind_of 1
boehmes@33419
  2553
    var t
boehmes@33419
  2554
      type-con $ctype 0
boehmes@33419
  2555
    fun $kind_primitive 0
boehmes@33419
  2556
axiom 0
boehmes@33419
  2557
    forall 1 1 4
boehmes@33419
  2558
      var t
boehmes@33419
  2559
        type-con $ctype 0
boehmes@33419
  2560
      pat 1
boehmes@33419
  2561
        fun $is_composite 1
boehmes@33419
  2562
        var t
boehmes@33419
  2563
          type-con $ctype 0
boehmes@33419
  2564
      attribute qid 1
boehmes@33419
  2565
        string-attr VccPrelu.173:36
boehmes@33419
  2566
      attribute uniqueId 1
boehmes@33419
  2567
        string-attr 11
boehmes@33419
  2568
      attribute bvZ3Native 1
boehmes@33419
  2569
        string-attr False
boehmes@33419
  2570
      attribute weight 1
boehmes@33419
  2571
        expr-attr
boehmes@33419
  2572
          int-num 0
boehmes@33419
  2573
    =
boehmes@33419
  2574
    fun $is_composite 1
boehmes@33419
  2575
    var t
boehmes@33419
  2576
      type-con $ctype 0
boehmes@33419
  2577
    =
boehmes@33419
  2578
    fun $kind_of 1
boehmes@33419
  2579
    var t
boehmes@33419
  2580
      type-con $ctype 0
boehmes@33419
  2581
    fun $kind_composite 0
boehmes@33419
  2582
axiom 0
boehmes@33419
  2583
    forall 1 1 4
boehmes@33419
  2584
      var t
boehmes@33419
  2585
        type-con $ctype 0
boehmes@33419
  2586
      pat 1
boehmes@33419
  2587
        fun $is_arraytype 1
boehmes@33419
  2588
        var t
boehmes@33419
  2589
          type-con $ctype 0
boehmes@33419
  2590
      attribute qid 1
boehmes@33419
  2591
        string-attr VccPrelu.179:36
boehmes@33419
  2592
      attribute uniqueId 1
boehmes@33419
  2593
        string-attr 12
boehmes@33419
  2594
      attribute bvZ3Native 1
boehmes@33419
  2595
        string-attr False
boehmes@33419
  2596
      attribute weight 1
boehmes@33419
  2597
        expr-attr
boehmes@33419
  2598
          int-num 0
boehmes@33419
  2599
    =
boehmes@33419
  2600
    fun $is_arraytype 1
boehmes@33419
  2601
    var t
boehmes@33419
  2602
      type-con $ctype 0
boehmes@33419
  2603
    =
boehmes@33419
  2604
    fun $kind_of 1
boehmes@33419
  2605
    var t
boehmes@33419
  2606
      type-con $ctype 0
boehmes@33419
  2607
    fun $kind_array 0
boehmes@33419
  2608
axiom 0
boehmes@33419
  2609
    forall 1 1 4
boehmes@33419
  2610
      var t
boehmes@33419
  2611
        type-con $ctype 0
boehmes@33419
  2612
      pat 1
boehmes@33419
  2613
        fun $is_threadtype 1
boehmes@33419
  2614
        var t
boehmes@33419
  2615
          type-con $ctype 0
boehmes@33419
  2616
      attribute qid 1
boehmes@33419
  2617
        string-attr VccPrelu.185:37
boehmes@33419
  2618
      attribute uniqueId 1
boehmes@33419
  2619
        string-attr 13
boehmes@33419
  2620
      attribute bvZ3Native 1
boehmes@33419
  2621
        string-attr False
boehmes@33419
  2622
      attribute weight 1
boehmes@33419
  2623
        expr-attr
boehmes@33419
  2624
          int-num 0
boehmes@33419
  2625
    =
boehmes@33419
  2626
    fun $is_threadtype 1
boehmes@33419
  2627
    var t
boehmes@33419
  2628
      type-con $ctype 0
boehmes@33419
  2629
    =
boehmes@33419
  2630
    fun $kind_of 1
boehmes@33419
  2631
    var t
boehmes@33419
  2632
      type-con $ctype 0
boehmes@33419
  2633
    fun $kind_thread 0
boehmes@33419
  2634
axiom 0
boehmes@33419
  2635
    forall 1 1 4
boehmes@33419
  2636
      var t
boehmes@33419
  2637
        type-con $ctype 0
boehmes@33419
  2638
      pat 1
boehmes@33419
  2639
        fun $is_composite 1
boehmes@33419
  2640
        var t
boehmes@33419
  2641
          type-con $ctype 0
boehmes@33419
  2642
      attribute qid 1
boehmes@33419
  2643
        string-attr VccPrelu.198:15
boehmes@33419
  2644
      attribute uniqueId 1
boehmes@33419
  2645
        string-attr 14
boehmes@33419
  2646
      attribute bvZ3Native 1
boehmes@33419
  2647
        string-attr False
boehmes@33419
  2648
      attribute weight 1
boehmes@33419
  2649
        expr-attr
boehmes@33419
  2650
          int-num 0
boehmes@33419
  2651
    implies
boehmes@33419
  2652
    fun $is_composite 1
boehmes@33419
  2653
    var t
boehmes@33419
  2654
      type-con $ctype 0
boehmes@33419
  2655
    fun $is_non_primitive 1
boehmes@33419
  2656
    var t
boehmes@33419
  2657
      type-con $ctype 0
boehmes@33419
  2658
axiom 0
boehmes@33419
  2659
    forall 1 1 4
boehmes@33419
  2660
      var t
boehmes@33419
  2661
        type-con $ctype 0
boehmes@33419
  2662
      pat 1
boehmes@33419
  2663
        fun $is_arraytype 1
boehmes@33419
  2664
        var t
boehmes@33419
  2665
          type-con $ctype 0
boehmes@33419
  2666
      attribute qid 1
boehmes@33419
  2667
        string-attr VccPrelu.199:15
boehmes@33419
  2668
      attribute uniqueId 1
boehmes@33419
  2669
        string-attr 15
boehmes@33419
  2670
      attribute bvZ3Native 1
boehmes@33419
  2671
        string-attr False
boehmes@33419
  2672
      attribute weight 1
boehmes@33419
  2673
        expr-attr
boehmes@33419
  2674
          int-num 0
boehmes@33419
  2675
    implies
boehmes@33419
  2676
    fun $is_arraytype 1
boehmes@33419
  2677
    var t
boehmes@33419
  2678
      type-con $ctype 0
boehmes@33419
  2679
    fun $is_non_primitive 1
boehmes@33419
  2680
    var t
boehmes@33419
  2681
      type-con $ctype 0
boehmes@33419
  2682
axiom 0
boehmes@33419
  2683
    forall 1 1 4
boehmes@33419
  2684
      var t
boehmes@33419
  2685
        type-con $ctype 0
boehmes@33419
  2686
      pat 1
boehmes@33419
  2687
        fun $is_threadtype 1
boehmes@33419
  2688
        var t
boehmes@33419
  2689
          type-con $ctype 0
boehmes@33419
  2690
      attribute qid 1
boehmes@33419
  2691
        string-attr VccPrelu.200:15
boehmes@33419
  2692
      attribute uniqueId 1
boehmes@33419
  2693
        string-attr 16
boehmes@33419
  2694
      attribute bvZ3Native 1
boehmes@33419
  2695
        string-attr False
boehmes@33419
  2696
      attribute weight 1
boehmes@33419
  2697
        expr-attr
boehmes@33419
  2698
          int-num 0
boehmes@33419
  2699
    implies
boehmes@33419
  2700
    fun $is_threadtype 1
boehmes@33419
  2701
    var t
boehmes@33419
  2702
      type-con $ctype 0
boehmes@33419
  2703
    fun $is_non_primitive 1
boehmes@33419
  2704
    var t
boehmes@33419
  2705
      type-con $ctype 0
boehmes@33419
  2706
axiom 0
boehmes@33419
  2707
    forall 2 1 3
boehmes@33419
  2708
      var #r
boehmes@33419
  2709
        type-con $ctype 0
boehmes@33419
  2710
      var #d
boehmes@33419
  2711
        type-con $ctype 0
boehmes@33419
  2712
      pat 1
boehmes@33419
  2713
        fun $map_t 2
boehmes@33419
  2714
        var #r
boehmes@33419
  2715
          type-con $ctype 0
boehmes@33419
  2716
        var #d
boehmes@33419
  2717
          type-con $ctype 0
boehmes@33419
  2718
      attribute qid 1
boehmes@33419
  2719
        string-attr VccPrelu.208:15
boehmes@33419
  2720
      attribute uniqueId 1
boehmes@33419
  2721
        string-attr 17
boehmes@33419
  2722
      attribute bvZ3Native 1
boehmes@33419
  2723
        string-attr False
boehmes@33419
  2724
    fun $is_primitive 1
boehmes@33419
  2725
    fun $map_t 2
boehmes@33419
  2726
    var #r
boehmes@33419
  2727
      type-con $ctype 0
boehmes@33419
  2728
    var #d
boehmes@33419
  2729
      type-con $ctype 0
boehmes@33419
  2730
axiom 0
boehmes@33419
  2731
    forall 1 1 3
boehmes@33419
  2732
      var #n
boehmes@33419
  2733
        type-con $ctype 0
boehmes@33419
  2734
      pat 1
boehmes@33419
  2735
        fun $ptr_to 1
boehmes@33419
  2736
        var #n
boehmes@33419
  2737
          type-con $ctype 0
boehmes@33419
  2738
      attribute qid 1
boehmes@33419
  2739
        string-attr VccPrelu.209:15
boehmes@33419
  2740
      attribute uniqueId 1
boehmes@33419
  2741
        string-attr 18
boehmes@33419
  2742
      attribute bvZ3Native 1
boehmes@33419
  2743
        string-attr False
boehmes@33419
  2744
    fun $is_primitive 1
boehmes@33419
  2745
    fun $ptr_to 1
boehmes@33419
  2746
    var #n
boehmes@33419
  2747
      type-con $ctype 0
boehmes@33419
  2748
axiom 0
boehmes@33419
  2749
    forall 1 1 3
boehmes@33419
  2750
      var #n
boehmes@33419
  2751
        type-con $ctype 0
boehmes@33419
  2752
      pat 1
boehmes@33419
  2753
        fun $is_primitive 1
boehmes@33419
  2754
        var #n
boehmes@33419
  2755
          type-con $ctype 0
boehmes@33419
  2756
      attribute qid 1
boehmes@33419
  2757
        string-attr VccPrelu.210:15
boehmes@33419
  2758
      attribute uniqueId 1
boehmes@33419
  2759
        string-attr 19
boehmes@33419
  2760
      attribute bvZ3Native 1
boehmes@33419
  2761
        string-attr False
boehmes@33419
  2762
    implies
boehmes@33419
  2763
    fun $is_primitive 1
boehmes@33419
  2764
    var #n
boehmes@33419
  2765
      type-con $ctype 0
boehmes@33419
  2766
    not
boehmes@33419
  2767
    fun $is_claimable 1
boehmes@33419
  2768
    var #n
boehmes@33419
  2769
      type-con $ctype 0
boehmes@33419
  2770
axiom 0
boehmes@33419
  2771
    fun $is_primitive 1
boehmes@33419
  2772
    fun ^^void 0
boehmes@33419
  2773
axiom 0
boehmes@33419
  2774
    fun $is_primitive 1
boehmes@33419
  2775
    fun ^^bool 0
boehmes@33419
  2776
axiom 0
boehmes@33419
  2777
    fun $is_primitive 1
boehmes@33419
  2778
    fun ^^mathint 0
boehmes@33419
  2779
axiom 0
boehmes@33419
  2780
    fun $is_primitive 1
boehmes@33419
  2781
    fun ^$#ptrset 0
boehmes@33419
  2782
axiom 0
boehmes@33419
  2783
    fun $is_primitive 1
boehmes@33419
  2784
    fun ^$#state_t 0
boehmes@33419
  2785
axiom 0
boehmes@33419
  2786
    fun $is_threadtype 1
boehmes@33419
  2787
    fun ^$#thread_id_t 0
boehmes@33419
  2788
axiom 0
boehmes@33419
  2789
    fun $is_primitive 1
boehmes@33419
  2790
    fun ^^i1 0
boehmes@33419
  2791
axiom 0
boehmes@33419
  2792
    fun $is_primitive 1
boehmes@33419
  2793
    fun ^^i2 0
boehmes@33419
  2794
axiom 0
boehmes@33419
  2795
    fun $is_primitive 1
boehmes@33419
  2796
    fun ^^i4 0
boehmes@33419
  2797
axiom 0
boehmes@33419
  2798
    fun $is_primitive 1
boehmes@33419
  2799
    fun ^^i8 0
boehmes@33419
  2800
axiom 0
boehmes@33419
  2801
    fun $is_primitive 1
boehmes@33419
  2802
    fun ^^u1 0
boehmes@33419
  2803
axiom 0
boehmes@33419
  2804
    fun $is_primitive 1
boehmes@33419
  2805
    fun ^^u2 0
boehmes@33419
  2806
axiom 0
boehmes@33419
  2807
    fun $is_primitive 1
boehmes@33419
  2808
    fun ^^u4 0
boehmes@33419
  2809
axiom 0
boehmes@33419
  2810
    fun $is_primitive 1
boehmes@33419
  2811
    fun ^^u8 0
boehmes@33419
  2812
axiom 0
boehmes@33419
  2813
    fun $is_primitive 1
boehmes@33419
  2814
    fun ^^f4 0
boehmes@33419
  2815
axiom 0
boehmes@33419
  2816
    fun $is_primitive 1
boehmes@33419
  2817
    fun ^^f8 0
boehmes@33419
  2818
axiom 0
boehmes@33419
  2819
    =
boehmes@33419
  2820
    fun $me 0
boehmes@33419
  2821
    fun $ptr 2
boehmes@33419
  2822
    fun ^$#thread_id_t 0
boehmes@33419
  2823
    fun $me_ref 0
boehmes@33419
  2824
axiom 0