16032530443

Committed 02 Jul 2025 06:08PM UTC coverage: 60.349% (-5.0%) from 65.357%

Build # 16032530443

Build Type

Pull #582

github

Committed by

web-flow

Commit Message

Merge b7e09d316 into b3af64ab1

Pull Request Pull Request #582: Update ci

Coverage Stats

63716 of 105580 relevant lines covered (60.35%)

1127640.75 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

87.5

/src/utils/int_hash_map.c

/*
 * This file is part of the Yices SMT Solver.
 * Copyright (C) 2017 SRI International.
 *
 * Yices is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * Yices is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
 */

/*
 * MAPS 32BIT INTEGERS TO 32BIT INTEGERS
 * Assumes that keys are non-negative
 */

#include <assert.h>

#include "utils/int_hash_map.h"
#include "utils/memalloc.h"


/*
 * For debugging: check whether n is 0 or a power of 2
 */
#ifndef NDEBUG
static bool is_power_of_two(uint32_t n) {
  return (n & (n - 1)) == 0;
}
#endif


/*
 * Initialization:
 * - n = initial size, must be a power of 2
 * - if n = 0, the default size is used
 */
void init_int_hmap(int_hmap_t *hmap, uint32_t n) {
  uint32_t i;
  int_hmap_pair_t *tmp;

  if (n == 0) {
    n = INT_HMAP_DEFAULT_SIZE;
  }

  if (n >= INT_HMAP_MAX_SIZE) {
    out_of_memory();
  }

  assert(is_power_of_two(n));

  tmp = (int_hmap_pair_t *) safe_malloc(n * sizeof(int_hmap_pair_t));
  for (i=0; i<n; i++) {
    tmp[i].key = EMPTY_KEY;
  }

  hmap->data = tmp;
  hmap->size = n;
  hmap->nelems = 0;
  hmap->ndeleted = 0;

  hmap->resize_threshold = (uint32_t)(n * INT_HMAP_RESIZE_RATIO);
  hmap->cleanup_threshold = (uint32_t) (n * INT_HMAP_CLEANUP_RATIO);
}


/*
 * Free memory
 */
void delete_int_hmap(int_hmap_t *hmap) {
  safe_free(hmap->data);
  hmap->data = NULL;
}


/*
 * Hash of a key (Jenkins hash)
 */
static uint32_t hash_key(int32_t k) {
  uint32_t x;

  x = (uint32_t) k;
  x = (x + 0x7ed55d16) + (x<<12);
  x = (x ^ 0xc761c23c) ^ (x>>19);
  x = (x + 0x165667b1) + (x<<5);
  x = (x + 0xd3a2646c) ^ (x<<9);
  x = (x + 0xfd7046c5) + (x<<3);
  x = (x ^ 0xb55a4f09) ^ (x>>16);

  return x;
}

/*
 * Make a copy of record d in a clean array data
 * - mask = size of data - 1 (size must be a power of 2)
 */
static void int_hmap_clean_copy(int_hmap_pair_t *data, int_hmap_pair_t *d, uint32_t mask) {
  uint32_t j;

  j = hash_key(d->key) & mask;
  while (data[j].key != EMPTY_KEY) {
    j ++;
    j &= mask;
  }

  data[j].key = d->key;
  data[j].val = d->val;
}


/*
 * Remove deleted records
 */
static void int_hmap_cleanup(int_hmap_t *hmap) {
  int_hmap_pair_t *tmp, *d;
  uint32_t j, n, mask;

  n = hmap->size;
  tmp = (int_hmap_pair_t *) safe_malloc(n * sizeof(int_hmap_pair_t));
  for (j=0; j<n; j++) {
    tmp[j].key = EMPTY_KEY;
  }

  mask = n - 1;
  d = hmap->data;
  for (j=0; j<n; j++) {
    if (d->key >= 0) {
      int_hmap_clean_copy(tmp, d, mask);
    }
    d++;
  }

  safe_free(hmap->data);
  hmap->data = tmp;
  hmap->ndeleted = 0;
}


/*
 * Remove deleted records and make the table twice as large
 */
static void int_hmap_extend(int_hmap_t *hmap) {
  int_hmap_pair_t *tmp, *d;
  uint32_t j, n, n2, mask;

  n = hmap->size;
  n2 = n << 1;
  if (n2 >= INT_HMAP_MAX_SIZE) {
    out_of_memory();
  }

  tmp = (int_hmap_pair_t *) safe_malloc(n2 * sizeof(int_hmap_pair_t));
  for (j=0; j<n2; j++) {
    tmp[j].key = EMPTY_KEY;
  }

  mask = n2 - 1;
  d = hmap->data;
  for (j=0; j<n; j++) {
    if (d->key >= 0) {
      int_hmap_clean_copy(tmp, d, mask);
    }
    d ++;
  }

  safe_free(hmap->data);
  hmap->data = tmp;
  hmap->size = n2;
  hmap->ndeleted = 0;

  hmap->resize_threshold = (uint32_t)(n2 * INT_HMAP_RESIZE_RATIO);
  hmap->cleanup_threshold = (uint32_t)(n2 * INT_HMAP_CLEANUP_RATIO);
}


/*
 * Find record with key k
 * - return NULL if k is not in the table
 */
int_hmap_pair_t *int_hmap_find(const int_hmap_t *hmap, int32_t k) {
  uint32_t mask, j;
  int_hmap_pair_t *d;

  assert(k >= 0);

  mask = hmap->size - 1;
  j = hash_key(k) & mask;
  for (;;) {
    d = hmap->data + j;
    if (d->key == k) return d;
    if (d->key == EMPTY_KEY) return NULL;
    j ++;
    j &= mask;
  }
}


/*
 * Add record with key k after hmap was extended:
 * - initialize val to -1
 * - we know that no record with key k is present
 */
static int_hmap_pair_t *int_hmap_get_clean(int_hmap_t *hmap, int32_t k) {
  uint32_t mask, j;
  int_hmap_pair_t *d;

  mask = hmap->size - 1;
  j = hash_key(k) & mask;
  for (;;) {
    d = hmap->data + j;
    if (d->key < 0) {
      hmap->nelems ++;
      d->key = k;
      d->val = -1;
      return d;
    }
    j ++;
    j &= mask;
  }
}


/*
 * Find or add record with key k
 */
int_hmap_pair_t *int_hmap_get(int_hmap_t *hmap, int32_t k) {
  uint32_t mask, j;
  int_hmap_pair_t *d, *aux;

  assert(k >= 0);
  assert(hmap->size > hmap->ndeleted + hmap->nelems);

  mask = hmap->size - 1;
  j = hash_key(k) & mask;

  for (;;) {
    d = hmap->data + j;
    if (d->key == k) return d;
    if (d->key < 0) break;
    j ++;
    j &= mask;
  }

  aux = d; // new record, if needed, will be aux
  while (d->key != EMPTY_KEY) {
    j ++;
    j &= mask;
    d = hmap->data + j;
    if (d->key == k) return d;
  }

  if (aux->key == DELETED_KEY) {
    assert(hmap->ndeleted > 0);
    hmap->ndeleted --;
  }

  if (hmap->nelems + hmap->ndeleted >= hmap->resize_threshold) {
    int_hmap_extend(hmap);
    aux = int_hmap_get_clean(hmap, k);
  } else {
    hmap->nelems ++;
    aux->key = k;
    aux->val = -1;
  }

  return aux;
}


/*
 * Add record [k -> v ] to hmap
 * - there must not be a record with the same key
 */
void int_hmap_add(int_hmap_t *hmap, int32_t k, int32_t v) {
  uint32_t i, mask;

  assert(k >= 0 && hmap->nelems + hmap->ndeleted < hmap->size);

  mask = hmap->size - 1;
  i = hash_key(k) & mask;
  while (hmap->data[i].key >= 0) {
    assert(hmap->data[i].key != k);
    i ++;
    i &= mask;
  }

  // store the new record in data[i]
  if (hmap->data[i].key == DELETED_KEY) {
    assert(hmap->ndeleted > 0);
    hmap->ndeleted --;
  }
  hmap->data[i].key = k;
  hmap->data[i].val = v;
  hmap->nelems ++;

  if (hmap->nelems + hmap->ndeleted >= hmap->resize_threshold) {
    int_hmap_extend(hmap);
  }
}


/*
 * Erase record r
 */
void int_hmap_erase(int_hmap_t *hmap, int_hmap_pair_t *r) {
  assert(int_hmap_find(hmap, r->key) == r);

  r->key = DELETED_KEY;
  hmap->nelems --;
  hmap->ndeleted ++;
  if (hmap->ndeleted >= hmap->cleanup_threshold) {
    int_hmap_cleanup(hmap);
  }
}


/*
 * Empty the map
 */
void int_hmap_reset(int_hmap_t *hmap) {
  uint32_t i, n;
  int_hmap_pair_t *d;

  n = hmap->size;
  d = hmap->data;
  for (i=0; i<n; i++) {
    d->key = EMPTY_KEY;
    d ++;
  }

  hmap->nelems = 0;
  hmap->ndeleted = 0;
}



/*
 * First non-empty record in the table, starting from p
 */
static const int_hmap_pair_t *int_hmap_get_next(const int_hmap_t *hmap, const int_hmap_pair_t *p) {
  int_hmap_pair_t *end;

  end = hmap->data + hmap->size;
  while (p < end) {
    if (p->key != EMPTY_KEY) return p;
    p ++;
  }

  return NULL;
}


/*
 * Get the first non-empty record or NULL if the table is empty
 */
int_hmap_pair_t *int_hmap_first_record(const int_hmap_t *hmap) {
  return (int_hmap_pair_t *) int_hmap_get_next(hmap, hmap->data);
}


/*
 * Next record after p or NULL
 */
int_hmap_pair_t *int_hmap_next_record(const int_hmap_t *hmap, const int_hmap_pair_t *p) {
  assert(p != NULL && p<hmap->data + hmap->size && p->key != EMPTY_KEY);
  return (int_hmap_pair_t *) int_hmap_get_next(hmap, p+1);
}




/*
 * Remove the records that satisfy filter f
 * - calls f(aux, p) on every record p stored in hmap
 * - if f(aux, p) returns true then record p is removed
 */
void int_hmap_remove_records(int_hmap_t *hmap, void *aux, int_hmap_filter_t f) {
  int_hmap_pair_t *d;
  uint32_t i, n, k;

  n = hmap->size;
  d = hmap->data;
  k = 0;
  for (i=0; i<n; i++) {
    if (d->key >= 0 && f(aux, d)) {
      // mark d as deleted
      d->key = DELETED_KEY;
      k ++;
    }
    d ++;
  }

  // k = number of deleted records
  assert(k <= hmap->nelems);
  hmap->nelems -= k;
  hmap->ndeleted += k;
  if (hmap->ndeleted >= hmap->cleanup_threshold) {
    int_hmap_cleanup(hmap);
  }
}



/*
 * Iterator: call f(aux, p) on every record p
 */
void int_hmap_iterate(int_hmap_t *hmap, void *aux, int_hmap_iterator_t f) {
  int_hmap_pair_t *d;
  uint32_t i, n;

  n = hmap->size;
  d = hmap->data;
  for (i=0; i<n; i++) {
    if (d->key >= 0) {
      f(aux, d);
    }
    d ++;
  }
}

1	/*
2	* This file is part of the Yices SMT Solver.
3	* Copyright (C) 2017 SRI International.
4	*
5	* Yices is free software: you can redistribute it and/or modify
6	* it under the terms of the GNU General Public License as published by
7	* the Free Software Foundation, either version 3 of the License, or
8	* (at your option) any later version.
9	*
10	* Yices is distributed in the hope that it will be useful,
11	* but WITHOUT ANY WARRANTY; without even the implied warranty of
12	* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13	* GNU General Public License for more details.
14	*
15	* You should have received a copy of the GNU General Public License
16	* along with Yices. If not, see <http://www.gnu.org/licenses/>.
17	*/
18
19	/*
20	* MAPS 32BIT INTEGERS TO 32BIT INTEGERS
21	* Assumes that keys are non-negative
22	*/
23
24	#include <assert.h>
25
26	#include "utils/int_hash_map.h"
27	#include "utils/memalloc.h"
28
29
30	/*
31	* For debugging: check whether n is 0 or a power of 2
32	*/
33	#ifndef NDEBUG
34	static bool is_power_of_two(uint32_t n) {
35	return (n & (n - 1)) == 0;
36	}
37	#endif
38
39
40	/*
41	* Initialization:
42	* - n = initial size, must be a power of 2
43	* - if n = 0, the default size is used
44	*/
45	void init_int_hmap(int_hmap_t *hmap, uint32_t n) {	267,472✔
46	uint32_t i;
47	int_hmap_pair_t *tmp;
48
49	if (n == 0) {	267,472✔
50	n = INT_HMAP_DEFAULT_SIZE;	252,287✔
51	}
52
53	if (n >= INT_HMAP_MAX_SIZE) {	267,472✔
54	out_of_memory();	×
55	}
56
57	assert(is_power_of_two(n));
58
59	tmp = (int_hmap_pair_t ) safe_malloc(n sizeof(int_hmap_pair_t));	267,472✔
60	for (i=0; i<n; i++) {	10,284,336✔
61	tmp[i].key = EMPTY_KEY;	10,016,864✔
62	}
63
64	hmap->data = tmp;	267,472✔
65	hmap->size = n;	267,472✔
66	hmap->nelems = 0;	267,472✔
67	hmap->ndeleted = 0;	267,472✔
68
69	hmap->resize_threshold = (uint32_t)(n * INT_HMAP_RESIZE_RATIO);	267,472✔
70	hmap->cleanup_threshold = (uint32_t) (n * INT_HMAP_CLEANUP_RATIO);	267,472✔
71	}	267,472✔
72
73
74	/*
75	* Free memory
76	*/
77	void delete_int_hmap(int_hmap_t *hmap) {	267,472✔
78	safe_free(hmap->data);	267,472✔
79	hmap->data = NULL;	267,472✔
80	}	267,472✔
81
82
83	/*
84	* Hash of a key (Jenkins hash)
85	*/
86	static uint32_t hash_key(int32_t k) {	22,757,554✔
87	uint32_t x;
88
89	x = (uint32_t) k;	22,757,554✔
90	x = (x + 0x7ed55d16) + (x<<12);	22,757,554✔
91	x = (x ^ 0xc761c23c) ^ (x>>19);	22,757,554✔
92	x = (x + 0x165667b1) + (x<<5);	22,757,554✔
93	x = (x + 0xd3a2646c) ^ (x<<9);	22,757,554✔
94	x = (x + 0xfd7046c5) + (x<<3);	22,757,554✔
95	x = (x ^ 0xb55a4f09) ^ (x>>16);	22,757,554✔
96
97	return x;	22,757,554✔
98	}
99
100	/*
101	* Make a copy of record d in a clean array data
102	* - mask = size of data - 1 (size must be a power of 2)
103	*/
104	static void int_hmap_clean_copy(int_hmap_pair_t data, int_hmap_pair_t d, uint32_t mask) {	2,943,745✔
105	uint32_t j;
106
107	j = hash_key(d->key) & mask;	2,943,745✔
108	while (data[j].key != EMPTY_KEY) {	3,566,813✔
109	j ++;	623,068✔
110	j &= mask;	623,068✔
111	}
112
113	data[j].key = d->key;	2,943,745✔
114	data[j].val = d->val;	2,943,745✔
115	}	2,943,745✔
116
117
118	/*
119	* Remove deleted records
120	*/
121	static void int_hmap_cleanup(int_hmap_t *hmap) {	8✔
122	int_hmap_pair_t tmp, d;
123	uint32_t j, n, mask;
124
125	n = hmap->size;	8✔
126	tmp = (int_hmap_pair_t ) safe_malloc(n sizeof(int_hmap_pair_t));	8✔
127	for (j=0; j<n; j++) {	264✔
128	tmp[j].key = EMPTY_KEY;	256✔
129	}
130
131	mask = n - 1;	8✔
132	d = hmap->data;	8✔
133	for (j=0; j<n; j++) {	264✔
134	if (d->key >= 0) {	256✔
135	int_hmap_clean_copy(tmp, d, mask);	4✔
136	}
137	d++;	256✔
138	}
139
140	safe_free(hmap->data);	8✔
141	hmap->data = tmp;	8✔
142	hmap->ndeleted = 0;	8✔
143	}	8✔
144
145
146	/*
147	* Remove deleted records and make the table twice as large
148	*/
149	static void int_hmap_extend(int_hmap_t *hmap) {	55,637✔
150	int_hmap_pair_t tmp, d;
151	uint32_t j, n, n2, mask;
152
153	n = hmap->size;	55,637✔
154	n2 = n << 1;	55,637✔
155	if (n2 >= INT_HMAP_MAX_SIZE) {	55,637✔
156	out_of_memory();	×
157	}
158
159	tmp = (int_hmap_pair_t ) safe_malloc(n2 sizeof(int_hmap_pair_t));	55,637✔
160	for (j=0; j<n2; j++) {	9,928,213✔
161	tmp[j].key = EMPTY_KEY;	9,872,576✔
162	}
163
164	mask = n2 - 1;	55,637✔
165	d = hmap->data;	55,637✔
166	for (j=0; j<n; j++) {	4,991,925✔
167	if (d->key >= 0) {	4,936,288✔
168	int_hmap_clean_copy(tmp, d, mask);	2,943,741✔
169	}
170	d ++;	4,936,288✔
171	}
172
173	safe_free(hmap->data);	55,637✔
174	hmap->data = tmp;	55,637✔
175	hmap->size = n2;	55,637✔
176	hmap->ndeleted = 0;	55,637✔
177
178	hmap->resize_threshold = (uint32_t)(n2 * INT_HMAP_RESIZE_RATIO);	55,637✔
179	hmap->cleanup_threshold = (uint32_t)(n2 * INT_HMAP_CLEANUP_RATIO);	55,637✔
180	}	55,637✔
181
182
183	/*
184	* Find record with key k
185	* - return NULL if k is not in the table
186	*/
187	int_hmap_pair_t int_hmap_find(const int_hmap_t hmap, int32_t k) {	15,199,114✔
188	uint32_t mask, j;
189	int_hmap_pair_t *d;
190
191	assert(k >= 0);
192
193	mask = hmap->size - 1;	15,199,114✔
194	j = hash_key(k) & mask;	15,199,114✔
195	for (;;) {
196	d = hmap->data + j;	18,566,516✔
197	if (d->key == k) return d;	18,566,516✔
198	if (d->key == EMPTY_KEY) return NULL;	15,992,757✔
199	j ++;	3,367,402✔
200	j &= mask;	3,367,402✔
201	}
202	}
203
204
205	/*
206	* Add record with key k after hmap was extended:
207	* - initialize val to -1
208	* - we know that no record with key k is present
209	*/
210	static int_hmap_pair_t int_hmap_get_clean(int_hmap_t hmap, int32_t k) {	55,637✔
211	uint32_t mask, j;
212	int_hmap_pair_t *d;
213
214	mask = hmap->size - 1;	55,637✔
215	j = hash_key(k) & mask;	55,637✔
216	for (;;) {
217	d = hmap->data + j;	93,508✔
218	if (d->key < 0) {	93,508✔
219	hmap->nelems ++;	55,637✔
220	d->key = k;	55,637✔
221	d->val = -1;	55,637✔
222	return d;	55,637✔
223	}
224	j ++;	37,871✔
225	j &= mask;	37,871✔
226	}
227	}
228
229
230	/*
231	* Find or add record with key k
232	*/
233	int_hmap_pair_t int_hmap_get(int_hmap_t hmap, int32_t k) {	4,557,376✔
234	uint32_t mask, j;
235	int_hmap_pair_t d, aux;
236
237	assert(k >= 0);
238	assert(hmap->size > hmap->ndeleted + hmap->nelems);
239
240	mask = hmap->size - 1;	4,557,376✔
241	j = hash_key(k) & mask;	4,557,376✔
242
243	for (;;) {
244	d = hmap->data + j;	7,594,660✔
245	if (d->key == k) return d;	7,594,660✔
246	if (d->key < 0) break;	6,697,001✔
247	j ++;	3,037,284✔
248	j &= mask;	3,037,284✔
249	}
250
251	aux = d; // new record, if needed, will be aux	3,659,717✔
252	while (d->key != EMPTY_KEY) {	3,659,717✔
253	j ++;	×
254	j &= mask;	×
255	d = hmap->data + j;	×
256	if (d->key == k) return d;	×
257	}
258
259	if (aux->key == DELETED_KEY) {	3,659,717✔
260	assert(hmap->ndeleted > 0);
261	hmap->ndeleted --;	×
262	}
263
264	if (hmap->nelems + hmap->ndeleted >= hmap->resize_threshold) {	3,659,717✔
265	int_hmap_extend(hmap);	55,637✔
266	aux = int_hmap_get_clean(hmap, k);	55,637✔
267	} else {
268	hmap->nelems ++;	3,604,080✔
269	aux->key = k;	3,604,080✔
270	aux->val = -1;	3,604,080✔
271	}
272
273	return aux;	3,659,717✔
274	}
275
276
277	/*
278	* Add record [k -> v ] to hmap
279	* - there must not be a record with the same key
280	*/
281	void int_hmap_add(int_hmap_t *hmap, int32_t k, int32_t v) {	1,682✔
282	uint32_t i, mask;
283
284	assert(k >= 0 && hmap->nelems + hmap->ndeleted < hmap->size);
285
286	mask = hmap->size - 1;	1,682✔
287	i = hash_key(k) & mask;	1,682✔
288	while (hmap->data[i].key >= 0) {	1,692✔
289	assert(hmap->data[i].key != k);
290	i ++;	10✔
291	i &= mask;	10✔
292	}
293
294	// store the new record in data[i]
295	if (hmap->data[i].key == DELETED_KEY) {	1,682✔
296	assert(hmap->ndeleted > 0);
297	hmap->ndeleted --;	4✔
298	}
299	hmap->data[i].key = k;	1,682✔
300	hmap->data[i].val = v;	1,682✔
301	hmap->nelems ++;	1,682✔
302
303	if (hmap->nelems + hmap->ndeleted >= hmap->resize_threshold) {	1,682✔
304	int_hmap_extend(hmap);	×
305	}
306	}	1,682✔
307
308
309	/*
310	* Erase record r
311	*/
312	void int_hmap_erase(int_hmap_t hmap, int_hmap_pair_t r) {	1,682✔
313	assert(int_hmap_find(hmap, r->key) == r);
314
315	r->key = DELETED_KEY;	1,682✔
316	hmap->nelems --;	1,682✔
317	hmap->ndeleted ++;	1,682✔
318	if (hmap->ndeleted >= hmap->cleanup_threshold) {	1,682✔
319	int_hmap_cleanup(hmap);	8✔
320	}
321	}	1,682✔
322
323
324	/*
325	* Empty the map
326	*/
327	void int_hmap_reset(int_hmap_t *hmap) {	95,449✔
328	uint32_t i, n;
329	int_hmap_pair_t *d;
330
331	n = hmap->size;	95,449✔
332	d = hmap->data;	95,449✔
333	for (i=0; i<n; i++) {	15,818,873✔
334	d->key = EMPTY_KEY;	15,723,424✔
335	d ++;	15,723,424✔
336	}
337
338	hmap->nelems = 0;	95,449✔
339	hmap->ndeleted = 0;	95,449✔
340	}	95,449✔
341
342
343
344	/*
345	* First non-empty record in the table, starting from p
346	*/
347	static const int_hmap_pair_t int_hmap_get_next(const int_hmap_t hmap, const int_hmap_pair_t *p) {	18,525✔
348	int_hmap_pair_t *end;
349
350	end = hmap->data + hmap->size;	18,525✔
351	while (p < end) {	189,517✔
352	if (p->key != EMPTY_KEY) return p;	184,869✔
353	p ++;	170,992✔
354	}
355
356	return NULL;	4,648✔
357	}
358
359
360	/*
361	* Get the first non-empty record or NULL if the table is empty
362	*/
363	int_hmap_pair_t int_hmap_first_record(const int_hmap_t hmap) {	5,655✔
364	return (int_hmap_pair_t *) int_hmap_get_next(hmap, hmap->data);	5,655✔
365	}
366
367
368	/*
369	* Next record after p or NULL
370	*/
371	int_hmap_pair_t int_hmap_next_record(const int_hmap_t hmap, const int_hmap_pair_t *p) {	12,870✔
372	assert(p != NULL && p<hmap->data + hmap->size && p->key != EMPTY_KEY);
373	return (int_hmap_pair_t *) int_hmap_get_next(hmap, p+1);	12,870✔
374	}
375
376
377
378
379	/*
380	* Remove the records that satisfy filter f
381	* - calls f(aux, p) on every record p stored in hmap
382	* - if f(aux, p) returns true then record p is removed
383	*/
384	void int_hmap_remove_records(int_hmap_t hmap, void aux, int_hmap_filter_t f) {	×
385	int_hmap_pair_t *d;
386	uint32_t i, n, k;
387
388	n = hmap->size;	×
389	d = hmap->data;	×
390	k = 0;	×
391	for (i=0; i<n; i++) {	×
392	if (d->key >= 0 && f(aux, d)) {	×
393	// mark d as deleted
394	d->key = DELETED_KEY;	×
395	k ++;	×
396	}
397	d ++;	×
398	}
399
400	// k = number of deleted records
401	assert(k <= hmap->nelems);
402	hmap->nelems -= k;	×
403	hmap->ndeleted += k;	×
404	if (hmap->ndeleted >= hmap->cleanup_threshold) {	×
405	int_hmap_cleanup(hmap);	×
406	}
407	}	×
408
409
410
411	/*
412	* Iterator: call f(aux, p) on every record p
413	*/
414	void int_hmap_iterate(int_hmap_t hmap, void aux, int_hmap_iterator_t f) {	9,036✔
415	int_hmap_pair_t *d;
416	uint32_t i, n;
417
418	n = hmap->size;	9,036✔
419	d = hmap->data;	9,036✔
420	for (i=0; i<n; i++) {	299,116✔
421	if (d->key >= 0) {	290,080✔
422	f(aux, d);	486✔
423	}
424	d ++;	290,080✔
425	}
426	}	9,036✔

SRI-CSL / yices2 / 16032530443

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous