max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(runtime/hash): use size_t instead of unsigned

Browse source
This commit is contained in:
Leonardo de Moura 2019-04-03 03:19:50 -07:00
parent 02e6f953c8
commit a46e27a3d7
2 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/runtime/hash.cpp
View file

@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <cstddef>
namespace lean {
void mix(unsigned & a, unsigned & b, unsigned & c) {
@ -20,8 +22,9 @@ void mix(unsigned & a, unsigned & b, unsigned & c) {
// Bob Jenkin's hash function.
// http://burtleburtle.net/bob/hash/doobs.html
unsigned hash_str(unsigned length, char const * str, unsigned init_value) {
unsigned a, b, c, len;
unsigned hash_str(size_t length, char const * str, unsigned init_value) {
unsigned a, b, c;
size_t len;
/* Set up the internal state */
len = length;

2
src/runtime/hash.h
View file

@ -12,7 +12,7 @@ namespace lean {
void mix(unsigned & a, unsigned & b, unsigned & c);
unsigned hash_str(unsigned len, char const * str, unsigned init_value);
unsigned hash_str(size_t len, char const * str, unsigned init_value);
inline unsigned hash(unsigned h1, unsigned h2) {
h2 -= h1; h2 ^= (h1 << 8);