--- layout: fc_discuss_archives title: Message 55 from Frama-C-discuss on May 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] String results in logical specifications



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