require g != null

This commit is contained in:
Alessandro Mauri 2026-03-20 18:25:54 +01:00
parent 14e0a6ad0a
commit f533d1f17a

View File

@ -107,9 +107,9 @@ fn usz Cache.get_free_spot(&cache)
return 0; return 0;
} }
<* @require g != null *>
fn Value*? Cache.insert_at(&cache, Value* g, Key id, usz index) fn Value*? Cache.insert_at(&cache, Value* g, Key id, usz index)
{ {
// TODO: verify index, g and id
Value* spot; Value* spot;
/* Set used and present */ /* Set used and present */
@ -124,12 +124,14 @@ fn Value*? Cache.insert_at(&cache, Value* g, Key id, usz index)
} }
// Insert an element in the cache, returns the index // Insert an element in the cache, returns the index
<* @require g != null *>
fn Value*? Cache.insert_new(&cache, Value* g, Key id) fn Value*? Cache.insert_new(&cache, Value* g, Key id)
{ {
usz index = cache.get_free_spot(); usz index = cache.get_free_spot();
return cache.insert_at(g, id, index); return cache.insert_at(g, id, index);
} }
<* @require g != null *>
fn Value*? Cache.get_or_insert(&cache, Value* g, Key id, bool *is_new = null) fn Value*? Cache.get_or_insert(&cache, Value* g, Key id, bool *is_new = null)
{ {
Value*? c = cache.search(id); Value*? c = cache.search(id);