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

  • Subject: [Frama-c-discuss] String results in logical specifications
  • From: amdunn at gmail.com (Alan Dunn)
  • Date: Fri, 22 May 2009 08:22:51 -0400
  • In-reply-to: <20090520175635.3837fc53@is005115>
  • References: <f90695ee0905130433g7040256ey5870d68dad50b48e@mail.gmail.com> <20090520175635.3837fc53@is005115>
Thanks for getting back to me. I have some further questions/comments.
(Thanks for humoring a newbie.)

> 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.

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...)

>> 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.

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

>>
>> 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.

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
it seems it can go slowly due to further tool bugs popping up

eg: I binary searched through my string axiomatization to find where
the following

[adunn at localhost strings]$ frama-c -jessie-analysis -jessie-behavior
default -jessie-gen-goals string_test.c
Parsing
[preprocessing] running gcc -C -E -I. -include
/usr/share/frama-c/jessie/jessie_prolog.h -dD string_test.c
Cleaning unused parts
Symbolic link
Starting semantical analysis
Starting Jessie translation
Producing Jessie files in subdir string_test.jessie
File string_test.jessie/string_test.jc written.
File string_test.jessie/string_test.cloc written.
Calling Jessie tool in subdir string_test.jessie
File "jc/jc_separation.ml", line 94, characters 28-28:
Uncaught exception: File "jc/jc_separation.ml", line 94, characters
28-34: Assertion failed
Jessie subprocess failed:    jessie  -why-opt -split-user-conj  -v
 -behavior default -locs string_test.cloc string_test.jc

occurs and found that in:

/*@ axiomatic Strings {
  @   type string;
  @   logic string string_of{L}(char *p);
  @   logic int string_length(string s);
  @
  @   predicate prestring_sensible{L}(char *p) =
  @     \exists int i; i >= 0 && \valid_range(p, 0, i) && *(p + i) == (char)0;
  @
  @   predicate prestring_length_at_least{L}(char *p, int i) =
  @     \valid_range(p, 0, i - 1) && (\forall int j; j <= i - 1 ==>
*(p + j) != (char)0);
  @
  @   axiom string_length_defining{L}:
  @     \forall char *p, int i; prestring_length_at_least{L}(p, i)
<==> string_length(string_of{L}(p)) >= i;
  @ }
  @*/

(where there are more definitions, but I stopped at the first error-causing one)

the part of the equivalence involving string_length and string_of is
the issue (it at least processes with no errors when replaces with
something trivial like 1 == 1).

Regardless of whether my logic is actually correct, it would be good
to be able to get to the level where I can examine the generated VCs
for functions involving this string axiomatization and examine them in
Coq and/or see if they can be proven with ATPs.

Again, I apologize if issues like the last need to be taken directly
to the Jessie crowd.

Is there some better way of doing this?

- Alan