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

Le ven. 22 mai 2009 08:22:51 CEST,
Alan Dunn <amdunn at gmail.com> a ?crit :
> 
> Ah - I got confused when I read the documentation from production
> "type-expr" in Figure 2.11 (in acsl-implementation-Lithium), which
> since seems to have changed names to "logic-type-expr" (in acsl_1.4) -
> that makes sense (though I suppose later examples should've clued me
> in...)

I don't remember precisely, but logic-type-expr is likely a
typo. 

> 
> Should I be mentioning issues like this on Why-discuss (as this is the
> origin of the Jessie tool)? Or filing bug reports?
> 

I have already opened a bug for that in Frama-C bts
(http://bts.frama-c.com/view.php?id=92). I forgot to tell you, sorry.
It does not seem to be a Why issue (Why is given an incorrect program
and is complaining about it), so I guess that Frama-C bts/mailing list
are suitable for the discussion, at least for now.

> It would be nice to be able to return strings from logical functions
> and to use more properties of strings than equality, so it seems like
> the former is a better idea. It certainly produces easier to read
> assertions. However, it seems like I would then have to duplicate a
> lot of the functionality that C string functions (which I'm having
> trouble using as strcmp, for example, seems to continue to give errors
> along the lines of what I mentioned before) should in theory take care
> of for me (eg: the evident one being that I have to axiomatize the
> length of such a string). Not that this is necessarily difficult, but

In fact, jessie/share/*.h already contain some axiomatization of
strings that you might find useful (I'm afraid it could be better
documented, though). In the mean time, we'll investigate the issue that
you reported for your own axiomatization.

Best regards,
-- 
Virgile Prevosto
Ing?nieur-Chercheur, CEA, LIST
Laboratoire de S?ret? des Logiciels
+33/0 1 69 08 71 83