- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
- 12
- 13
- 14
- 15
- 16
- 17
- 18
- 19
- 20
- 21
- 22
- 23
- 24
- 25
- 26
- 27
- 28
- 29
- 30
- 31
- 32
- 33
- 34
- 35
- 36
- 37
- 38
- 39
- 40
- 41
- 42
- 43
// https://github.com/CVC4/CVC4/blob/14b9dbaa0c9e8dce52d1a28595dc1cc80756abed/src/expr/pickler.cpp
static Block mkBlockBody4Chars(char a, char b, char c, char d) {
Block newBody;
newBody.d_body.d_data = (a << 24) | (b << 16) | (c << 8) | d;
return newBody;
}
static char getCharBlockBody(BlockBody body, int i) {
Assert(0 <= i && i <= 3);
switch(i) {
case 0: return (body.d_data & 0xff000000) >> 24;
case 1: return (body.d_data & 0x00ff0000) >> 16;
case 2: return (body.d_data & 0x0000ff00) >> 8;
case 3: return (body.d_data & 0x000000ff);
default:
Unreachable();
}
return '\0';
}
// ...
void PicklerPrivate::toCaseString(Kind k, const std::string& s) {
d_current << mkConstantHeader(k, s.size());
unsigned size = s.size();
unsigned i;
for(i = 0; i + 4 <= size; i += 4) {
d_current << mkBlockBody4Chars(s[i + 0], s[i + 1],s[i + 2], s[i + 3]);
}
switch(size % 4) {
case 0: break;
case 1: d_current << mkBlockBody4Chars(s[i + 0], '\0','\0', '\0'); break;
case 2: d_current << mkBlockBody4Chars(s[i + 0], s[i + 1], '\0', '\0'); break;
case 3: d_current << mkBlockBody4Chars(s[i + 0], s[i + 1],s[i + 2], '\0'); break;
default:
Unreachable();
}
}
Очередное переизобретение какой-то байтоебской поеботы типа ntohl(). И вообще, тут UB.