--- layout: fc_discuss_archives title: Message 55 from Frama-C-discuss on May 2009 ---
Hello Alan, Le mer. 13 mai 2009 07:33:22 CEST, Alan Dunn <amdunn at gmail.com> a ?crit : > > It seems that in the ACSL documentation there is no way to actually > create a logical function that returns something like a (char *) (only In theory, any C type is accepted in annotations. However, pointers that cannot be related to an object in the "C world" (such as the return value of your logical function) are indeed a bit problematic. Their status is not completely clear yet. > Calling Jessie tool in subdir pam_unix_auth.jessie Any error message past this line should be treated as a bug: the Jessie plugin (or the Jessie tool) is giving Why a bogus program. I'll let better experts than me comment on this specific Why error, though. > > Is there currently a good way of handling this? I can see either: > 1) Defining a "string" axiomatic type > 2) Folding all of my char * returning logical functions into > predicates on two (char *)'s eg: Both approaches should be fine. The first one might be a bit easier to use (you'll still have string object that you can manipulate), but I guess it's mostly a matter of taste at this point. Best regards, -- E tutto per oggi, a la prossima volta. Virgile