Model non-deterministic value integer in Frama-C

Could anyone please tell me is this the right model for non-deterministic values of integer and unsigned integer in Frama-C?

/* Suppose Frama-C is installed in /usr/local -default prefix */
#include "/usr/local/share/frama-c/builtin.h"
#include "/usr/local/share/frama-c/libc/limits.h"

...
#define nondet_int() Frama_C_interval(INT_MIN, INT_MAX)
#define nondet_uint() Frama_C_interval(0, UINT_MAX)
...

Are there any exceptions if I use the above code with different architectures in option -machdep?

Solution

One reason Frama_C_interval(0, UINT_MAX) may not work as intended is that Frama_C_interval has type int (int, int). When you happen to want the entire range of unsigned int values, that actually tends to help because the conversions that are introduced are subject to approximation, but in general the fact that Frama_C_interval is declared as returning an int is a nuisance.

The latest released version already has Frama_C_unsigned_int_interval, but it is in share/libc/__fc_builtin.h (installed to /usr/local/share/frama-c/libc/__fc_builtin.h. The file builtin.h looks like a vestigial remnant, especially with the $Id$ line dating back to when development was done under SVN.

For specifying that a value should be all possible unsigned intvalues, Frama_C_unsigned_int_interval(0, -1) saves yourself the trouble of including limit.h. The int value -1 passed as argument is converted to the largest unsigned int as per C rules.