/* Frama-C erzeugt eine komische Assertion über Zeigervergleiche für
 * diesen Code wenn man den value analyzer laufen lässt. Ist das ein
 * Programmfehler in Frama-C? */

#include <limits.h>
#include "/home/rcl/.opam/system/share/frama-c/builtin.h"

int main()
{
	const unsigned n = 10;
	int arr[n], val = 0;

	if (arr[0] == val)
		Frama_C_abort();

	return 0;
}

/*
 * The Frama-C value analyzer generate a weird assertion about pointer
 * comparisons for this code. Is this a programming error in Frama-C?
 * Invoke Frama-C like this:
 *
 *     frama-c-gui -val ptrcmp.c
 *
 * The generated assertion is:
 *
 *     \pointer_comparable((void *)*(arr+0), (void *)val);
 */

#include <limits.h>

int main()
{
	const unsigned n = 10;
	int arr[n], val = 0;

	if (arr[0] == val)
		Frama_C_abort();

	return 0;
}