/ Check-in [9a9627e1]
Login

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Add some requirements marks to the record formatting logic. Comment changes only - the code is unaltered.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1: 9a9627e178a67bbfc85366aaea900e674d22fb53
User & Date: drh 2014-11-20 02:18:14
Context
2014-11-20
02:58
Fix the encoding of some integers to use the minimum amount of space: -128, -32768, -8388608, -217483648, and -140737488355328. check-in: 2d7c8da5 user: drh tags: trunk
02:18
Add some requirements marks to the record formatting logic. Comment changes only - the code is unaltered. check-in: 9a9627e1 user: drh tags: trunk
2014-11-19
16:36
Add new requirements marks associated with the file format documentation. No changes to code. check-in: 6d00bcca user: drh tags: trunk
Changes
Hide Diffs Side-by-Side Diffs Ignore Whitespace Patch

Changes to src/vdbe.c.

  2632   2632       }
  2633   2633       nData += len;
  2634   2634       testcase( serial_type==127 );
  2635   2635       testcase( serial_type==128 );
  2636   2636       nHdr += serial_type<=127 ? 1 : sqlite3VarintLen(serial_type);
  2637   2637     }while( (--pRec)>=pData0 );
  2638   2638   
  2639         -  /* Add the initial header varint and total the size */
         2639  +  /* EVIDENCE-OF: R-22564-11647 The header begins with a single varint
         2640  +  ** which determines the total number of bytes in the header. The varint
         2641  +  ** value is the size of the header in bytes including the size varint
         2642  +  ** itself. */
  2640   2643     testcase( nHdr==126 );
  2641   2644     testcase( nHdr==127 );
  2642   2645     if( nHdr<=126 ){
  2643   2646       /* The common case */
  2644   2647       nHdr += 1;
  2645   2648     }else{
  2646   2649       /* Rare case of a really large header */
................................................................................
  2666   2669     /* Write the record */
  2667   2670     i = putVarint32(zNewRecord, nHdr);
  2668   2671     j = nHdr;
  2669   2672     assert( pData0<=pLast );
  2670   2673     pRec = pData0;
  2671   2674     do{
  2672   2675       serial_type = pRec->uTemp;
         2676  +    /* EVIDENCE-OF: R-06529-47362 Following the size varint are one or more
         2677  +    ** additional varints, one per column. */
  2673   2678       i += putVarint32(&zNewRecord[i], serial_type);            /* serial type */
         2679  +    /* EVIDENCE-OF: R-64536-51728 The values for each column in the record
         2680  +    ** immediately follow the header. */
  2674   2681       j += sqlite3VdbeSerialPut(&zNewRecord[j], pRec, serial_type); /* content */
  2675   2682     }while( (++pRec)<=pLast );
  2676   2683     assert( i==nHdr );
  2677   2684     assert( j==nByte );
  2678   2685   
  2679   2686     assert( pOp->p3>0 && pOp->p3<=(p->nMem-p->nCursor) );
  2680   2687     pOut->n = (int)nByte;

Changes to src/vdbeaux.c.

  3047   3047     u32 serial_type,              /* Serial type to deserialize */
  3048   3048     Mem *pMem                     /* Memory cell to write value into */
  3049   3049   ){
  3050   3050     u64 x = FOUR_BYTE_UINT(buf);
  3051   3051     u32 y = FOUR_BYTE_UINT(buf+4);
  3052   3052     x = (x<<32) + y;
  3053   3053     if( serial_type==6 ){
         3054  +    /* EVIDENCE-OF: R-29851-52272 Value is a big-endian 64-bit
         3055  +    ** twos-complement integer. */
  3054   3056       pMem->u.i = *(i64*)&x;
  3055   3057       pMem->flags = MEM_Int;
  3056   3058       testcase( pMem->u.i<0 );
  3057   3059     }else{
         3060  +    /* EVIDENCE-OF: R-57343-49114 Value is a big-endian IEEE 754-2008 64-bit
         3061  +    ** floating point number. */
  3058   3062   #if !defined(NDEBUG) && !defined(SQLITE_OMIT_FLOATING_POINT)
  3059   3063       /* Verify that integers and floating point values use the same
  3060   3064       ** byte order.  Or, that if SQLITE_MIXED_ENDIAN_64BIT_FLOAT is
  3061   3065       ** defined that 64-bit floating point values really are mixed
  3062   3066       ** endian.
  3063   3067       */
  3064   3068       static const u64 t1 = ((u64)0x3ff00000)<<32;
................................................................................
  3078   3082     const unsigned char *buf,     /* Buffer to deserialize from */
  3079   3083     u32 serial_type,              /* Serial type to deserialize */
  3080   3084     Mem *pMem                     /* Memory cell to write value into */
  3081   3085   ){
  3082   3086     switch( serial_type ){
  3083   3087       case 10:   /* Reserved for future use */
  3084   3088       case 11:   /* Reserved for future use */
  3085         -    case 0: {  /* NULL */
         3089  +    case 0: {  /* Null */
         3090  +      /* EVIDENCE-OF: R-24078-09375 Value is a NULL. */
  3086   3091         pMem->flags = MEM_Null;
  3087   3092         break;
  3088   3093       }
  3089         -    case 1: { /* 1-byte signed integer */
         3094  +    case 1: {
         3095  +      /* EVIDENCE-OF: R-44885-25196 Value is an 8-bit twos-complement
         3096  +      ** integer. */
  3090   3097         pMem->u.i = ONE_BYTE_INT(buf);
  3091   3098         pMem->flags = MEM_Int;
  3092   3099         testcase( pMem->u.i<0 );
  3093   3100         return 1;
  3094   3101       }
  3095   3102       case 2: { /* 2-byte signed integer */
         3103  +      /* EVIDENCE-OF: R-49794-35026 Value is a big-endian 16-bit
         3104  +      ** twos-complement integer. */
  3096   3105         pMem->u.i = TWO_BYTE_INT(buf);
  3097   3106         pMem->flags = MEM_Int;
  3098   3107         testcase( pMem->u.i<0 );
  3099   3108         return 2;
  3100   3109       }
  3101   3110       case 3: { /* 3-byte signed integer */
         3111  +      /* EVIDENCE-OF: R-37839-54301 Value is a big-endian 24-bit
         3112  +      ** twos-complement integer. */
  3102   3113         pMem->u.i = THREE_BYTE_INT(buf);
  3103   3114         pMem->flags = MEM_Int;
  3104   3115         testcase( pMem->u.i<0 );
  3105   3116         return 3;
  3106   3117       }
  3107   3118       case 4: { /* 4-byte signed integer */
         3119  +      /* EVIDENCE-OF: R-01849-26079 Value is a big-endian 32-bit
         3120  +      ** twos-complement integer. */
  3108   3121         pMem->u.i = FOUR_BYTE_INT(buf);
  3109   3122         pMem->flags = MEM_Int;
  3110   3123         testcase( pMem->u.i<0 );
  3111   3124         return 4;
  3112   3125       }
  3113   3126       case 5: { /* 6-byte signed integer */
         3127  +      /* EVIDENCE-OF: R-50385-09674 Value is a big-endian 48-bit
         3128  +      ** twos-complement integer. */
  3114   3129         pMem->u.i = FOUR_BYTE_UINT(buf+2) + (((i64)1)<<32)*TWO_BYTE_INT(buf);
  3115   3130         pMem->flags = MEM_Int;
  3116   3131         testcase( pMem->u.i<0 );
  3117   3132         return 6;
  3118   3133       }
  3119   3134       case 6:   /* 8-byte signed integer */
  3120   3135       case 7: { /* IEEE floating point */
  3121   3136         /* These use local variables, so do them in a separate routine
  3122   3137         ** to avoid having to move the frame pointer in the common case */
  3123   3138         return serialGet(buf,serial_type,pMem);
  3124   3139       }
  3125   3140       case 8:    /* Integer 0 */
  3126   3141       case 9: {  /* Integer 1 */
         3142  +      /* EVIDENCE-OF: R-12976-22893 Value is the integer 0. */
         3143  +      /* EVIDENCE-OF: R-18143-12121 Value is the integer 1. */
  3127   3144         pMem->u.i = serial_type-8;
  3128   3145         pMem->flags = MEM_Int;
  3129   3146         return 0;
  3130   3147       }
  3131   3148       default: {
         3149  +      /* EVIDENCE-OF: R-14606-31564 Value is a BLOB that is (N-12)/2 bytes in
         3150  +      ** length.
         3151  +      ** EVIDENCE-OF: R-28401-00140 Value is a string in the text encoding and
         3152  +      ** (N-13)/2 bytes in length. */
  3132   3153         static const u16 aFlag[] = { MEM_Blob|MEM_Ephem, MEM_Str|MEM_Ephem };
  3133   3154         pMem->z = (char *)buf;
  3134   3155         pMem->n = (serial_type-12)/2;
  3135   3156         pMem->flags = aFlag[serial_type&1];
  3136   3157         return pMem->n;
  3137   3158       }
  3138   3159     }