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] Axiomatic Definitions

  • Subject: [Frama-c-discuss] Axiomatic Definitions
  • From: yannick.moy at (Yannick Moy)
  • Date: Mon Nov 3 15:17:26 2008
  • In-reply-to: <26B6531824874E4094E89611CE0CCE8F@AHARDPLACE>
  • References: <EB35E997FEE7481CA9897244C5ABB940@AHARDPLACE> <> <26B6531824874E4094E89611CE0CCE8F@AHARDPLACE>


Existing solutions for recursively defined logic functions were not

- recursive logic function may very easily be ill-defined, in particular
when they should be defined only for some arguments, and left unspecified
for others (e.g., the length of a list), leading to inconsistencies.
For example, the following "natural" definition is wrong:

//@ logic integer list_length(List *x) = (x == NULL) ? 0 :
list_length(x->next) + 1;

By examining the case where x == x->next, it is possible to deduce that 0 ==

- reads clauses are likewise easily ill-written, leading to other
inconsistencies with axioms defining the function.
For example, the following reads clause is wrong:

//@ logic integer list_length(List *x) read x, x->next;

This does not take into account x->next->next, etc.

Our solution is to group together the declaration of a logic function
together with axioms that define it, in a axiomatic. Then, the reads clause
is automatically inferred from axioms. This is what is done for NbOcc
axiomatic, around nb_occ logic function. The same is true for predicates, or
various logic functions and predicates defined by a set of axioms.


On Mon, Nov 3, 2008 at 2:51 PM, Christoph Weber <> wrote:

>  Thanks for the example, that helps a lot. Funny that you discovered an
> error, I wasn't even aware of it :).
> I realize that the given axiomatic predicate will work. My Problem is
> why???
> Don't I have to define a function body or something like it and
> how will it be processed?
> In some examples I came across a reads[] clause, is this necessary or what
> does it do?
> You see I am confused.
> Cheers
> Christoph
> ----- Original Message -----
> *From:* Yannick Moy <>
> *To:* Christoph Weber <>
> *Cc:*
> *Sent:* Monday, November 03, 2008 2:16 PM
> *Subject:* Re: [Frama-c-discuss] Axiomatic Definitions
> Hi,
> You were right, there is indeed a typo in the version of NbOcc axiomatic
> present in ACSL manual ("i" is used twice where "j" is expected). The file
> in attachment is a correct version of NbOcc axiomatic as well as a counting
> C function that expresses such a property in its loop invariant and
> postcondition. All 4 of Alt-Ergo, Simplify, Z3 and Yices completely prove
> the generated VC.
> As I said, there are some issues with our memory model in the Jessie plugin
> that I cannot decide alone, therefore we must delay an answer to your
> previous mail to wednesday or thursday, depending on when we finally can
> meet to discuss this problem. Sorry for this inconvenience.
> Best regards,
> Yannick
> On Mon, Nov 3, 2008 at 1:06 PM, Christoph Weber <
>> wrote:
>>  Hello,
>> I studied the most recent ACSL 1.4 Manual. But I still don't know how to
>> program with it.
>> I would appreciate a working implementation of the "nbocc()" function.
>> By the way I would like to know when to expect a patch, to repair the
>> problem with loop verification.
>> Thanks in advance
>> Christoph
>> _______________________________________________
>> Frama-c-discuss mailing list
> --
> Yannick

-------------- next part --------------
An HTML attachment was scrubbed...