@@ -367,58 +367,58 @@ module C-COMMON-EXPR-RELATIONAL
367
367
rule tv(encodedPtr(Loc:SymLoc, N:Int, M:Int), T::UType) >= tv(encodedPtr(Loc':SymLoc, N:Int, M:Int), T'::UType)
368
368
=> tv(Loc, T) >= tv(Loc', T')
369
369
370
- rule tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), T ::UType) == tv(I:Int, T'::UType)
370
+ rule tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), _T ::UType) == tv(I:Int, T'::UType)
371
371
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T'))
372
- rule tv((L:SymLoc => unknown(maxIntPtrValue(L))), T ::UType) == tv(I:Int, T'::UType)
372
+ rule tv((L:SymLoc => unknown(maxIntPtrValue(L))), _T ::UType) == tv(I:Int, T'::UType)
373
373
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T'))
374
- rule tv(I:Int, T::UType) == tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), T '::UType)
374
+ rule tv(I:Int, T::UType) == tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), _T '::UType)
375
375
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T))
376
- rule tv(I:Int, T::UType) == tv((L:SymLoc => unknown(maxIntPtrValue(L))), T '::UType)
376
+ rule tv(I:Int, T::UType) == tv((L:SymLoc => unknown(maxIntPtrValue(L))), _T '::UType)
377
377
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T))
378
378
379
- rule tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), T ::UType) != tv(I:Int, T'::UType)
379
+ rule tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), _T ::UType) != tv(I:Int, T'::UType)
380
380
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T'))
381
- rule tv((L:SymLoc => unknown(maxIntPtrValue(L))), T ::UType) != tv(I:Int, T'::UType)
381
+ rule tv((L:SymLoc => unknown(maxIntPtrValue(L))), _T ::UType) != tv(I:Int, T'::UType)
382
382
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T'))
383
- rule tv(I:Int, T::UType) != tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), T '::UType)
383
+ rule tv(I:Int, T::UType) != tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), _T '::UType)
384
384
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T))
385
- rule tv(I:Int, T::UType) != tv((L:SymLoc => unknown(maxIntPtrValue(L))), T '::UType)
385
+ rule tv(I:Int, T::UType) != tv((L:SymLoc => unknown(maxIntPtrValue(L))), _T '::UType)
386
386
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T))
387
387
388
- rule tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), T ::UType) < tv(I:Int, T'::UType)
388
+ rule tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), _T ::UType) < tv(I:Int, T'::UType)
389
389
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T'))
390
- rule tv((L:SymLoc => unknown(maxIntPtrValue(L))), T ::UType) < tv(I:Int, T'::UType)
390
+ rule tv((L:SymLoc => unknown(maxIntPtrValue(L))), _T ::UType) < tv(I:Int, T'::UType)
391
391
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T'))
392
- rule tv(I:Int, T::UType) < tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), T '::UType)
392
+ rule tv(I:Int, T::UType) < tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), _T '::UType)
393
393
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T))
394
- rule tv(I:Int, T::UType) < tv((L:SymLoc => unknown(maxIntPtrValue(L))), T '::UType)
394
+ rule tv(I:Int, T::UType) < tv((L:SymLoc => unknown(maxIntPtrValue(L))), _T '::UType)
395
395
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T))
396
396
397
- rule tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), T ::UType) <= tv(I:Int, T'::UType)
397
+ rule tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), _T ::UType) <= tv(I:Int, T'::UType)
398
398
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T'))
399
- rule tv((L:SymLoc => unknown(maxIntPtrValue(L))), T ::UType) <= tv(I:Int, T'::UType)
399
+ rule tv((L:SymLoc => unknown(maxIntPtrValue(L))), _T ::UType) <= tv(I:Int, T'::UType)
400
400
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T'))
401
- rule tv(I:Int, T::UType) <= tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), T '::UType)
401
+ rule tv(I:Int, T::UType) <= tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), _T '::UType)
402
402
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T))
403
- rule tv(I:Int, T::UType) <= tv((L:SymLoc => unknown(maxIntPtrValue(L))), T '::UType)
403
+ rule tv(I:Int, T::UType) <= tv((L:SymLoc => unknown(maxIntPtrValue(L))), _T '::UType)
404
404
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T))
405
405
406
- rule tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), T ::UType) > tv(I:Int, T'::UType)
406
+ rule tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), _T ::UType) > tv(I:Int, T'::UType)
407
407
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T'))
408
- rule tv((L:SymLoc => unknown(maxIntPtrValue(L))), T ::UType) > tv(I:Int, T'::UType)
408
+ rule tv((L:SymLoc => unknown(maxIntPtrValue(L))), _T ::UType) > tv(I:Int, T'::UType)
409
409
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T'))
410
- rule tv(I:Int, T::UType) > tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), T '::UType)
410
+ rule tv(I:Int, T::UType) > tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), _T '::UType)
411
411
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T))
412
- rule tv(I:Int, T::UType) > tv((L:SymLoc => unknown(maxIntPtrValue(L))), T '::UType)
412
+ rule tv(I:Int, T::UType) > tv((L:SymLoc => unknown(maxIntPtrValue(L))), _T '::UType)
413
413
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T))
414
414
415
- rule tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), T ::UType) >= tv(I:Int, T'::UType)
415
+ rule tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), _T ::UType) >= tv(I:Int, T'::UType)
416
416
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T'))
417
- rule tv((L:SymLoc => unknown(maxIntPtrValue(L))), T ::UType) >= tv(I:Int, T'::UType)
417
+ rule tv((L:SymLoc => unknown(maxIntPtrValue(L))), _T ::UType) >= tv(I:Int, T'::UType)
418
418
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T'))
419
- rule tv(I:Int, T::UType) >= tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), T '::UType)
419
+ rule tv(I:Int, T::UType) >= tv((encodedPtr(L:SymLoc, N::Int, M::Int) => unknown(maxIntPtrValue(encodedPtr(L, N, M)))), _T '::UType)
420
420
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T))
421
- rule tv(I:Int, T::UType) >= tv((L:SymLoc => unknown(maxIntPtrValue(L))), T '::UType)
421
+ rule tv(I:Int, T::UType) >= tv((L:SymLoc => unknown(maxIntPtrValue(L))), _T '::UType)
422
422
requires L =/=K NullPointer andBool notBool isNullPointerConstant(tv(I, T))
423
423
424
424
rule tv((encodedPtr(NullPointer, _, _) => unknown(0)), _) == tv(_:Int, _)
0 commit comments