Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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