--- layout: fc_discuss_archives title: Message 105 from Frama-C-discuss on September 2013 ---
On Mon, Sep 16, 2013 at 1:39 AM, Stephen Siegel <siegel at udel.edu> wrote: > > I guess you could obtain something like this using a function > "chooseBool()" which returns a boolean and which is totally unconstrained, > and use that as the condition in an "if" statement. Or you could use a > function "chooseInt()" with a switch statement. > > You will find contracts for functions Frama_C_interval() and Frama_C_nondet() in __fc_builtin.h: extern int Frama_C_entropy_source; /*@ assigns \result \from a, b, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; ensures \result == a || \result == b ; */ int Frama_C_nondet(int a, int b); /*@ assigns \result \from min, max, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; ensures min <= \result <= max ; */ int Frama_C_interval(int min, int max); -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130916/e2fb47b5/attachment.html>