shttpd/lex/findchar.c

// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
// Copyright © 2019 Ariadne Devos

#include <sHT/index.h>
#include <sHT/lex/findchar.h>

#include <stddef.h>
#include <stdint.h>

size_t
sHT_findchar(size_t e, const uint8_t from[e], size_t b, const sHT_charclass s)
{
	size_t i = b;
	if (sHT_ge(i, e))
		return i;
	/*@ loop invariant rINS: b <= i < e;
	    loop invariant rIS: b <= e;
	    loop invariant before_INS: \forall ℤ j; b <= j < i ==> !in_charclass(s, from[j]);
	    loop assigns i;
	    loop variant e - i; */
	do {	i = sHT_index_nospec(i, e);
		if (sHT_charclass_test(s, from[i]))
			break;
		/*@ assert !in_charclass(s, from[i]); */
		i++;
	} while (sHT_lt(i, e));
	return i;
}