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] The && operator in logical annotations

  • Subject: [Frama-c-discuss] The && operator in logical annotations
  • From: yannick.moy at gmail.com (Yannick Moy)
  • Date: Mon Aug 4 18:43:18 2008
Hi,

The following message was sent on the Why discussion list. I think the issue
it raises should be discussed here. This has to do with the different
meaning of && in logical annotations and in C code. In the example below,
this causes an inversion of priority between operators in code and logical
annotations, which is rather confusing.

There is sometimes a solution which consists in writing equivalences instead
of equality for booleans:
ensures C->O0 <==> C->I1 && C->I0;
instead of
ensures C->O0 == C->I1 && C->I0;

but it is not always possible. Therefore I tried in Frama-C to cast the
boolen into an integer, but it is refused:
ensures C->O0 == (int)(C->I1 && C->I0);
with an error:
Error: Casting from type boolean to type int  not allowed

However, the ACSL documentation indicates it should be possible. Is it
future work?

Concerning the problem of different semantics and priority for && in code
and annotations, Jonathan Shapiro answered on the Why list:

This is a sufficiently bad intrusion into C expressions that the logical
> annotation language would do well to change keywords.
>

What about this proposal?

Yannick


---------- Forwarded message ----------
From: <jean-baptiste.jeannin@hispano-suiza-sa.com>
Date: Mon, Aug 4, 2008 at 11:40 AM
Subject: [Why-discuss] The && operator in Caduceus
To: Why-discuss@lists.gforge.inria.fr



Good morning,

In this question I am talking about the operator && in C (logical AND
between entities of type int).

Let us say I am trying to prove, using Caduceus, the following program:

typedef struct {
int I0;
int I1;
int O0;
} T;

void ComputeCommands (T *C){
C->O0 = (C->I1) && (C->I0);
}

The first thing I did was to annotate the program in the following way:

typedef struct {
int I0;
int I1;
int O0;
} T;

/*@ requires \valid(C)
  @ assigns C->O0
  @ ensures C->O0 == C->I1 && C->I0
  @*/
void ComputeCommands (T *C){
C->O0 = (C->I1) && (C->I0);
}

However after some analysis of the generated conditions (since they require
C->I0 to be different from 0), it looks like the ensures condition is
interpreted as "(C->O0 == C->I1) && C->I0" rather than as "C->O0 == C->I1 &&
C->I0" as I expected. Is it normal, here, that the priority of == is less
than the one of && ? it was confusing since && is of smaller priority than =
(the assignment operator) in the code.

Then I put the required parenthesis like this:

typedef struct {
int I0;
int I1;
int O0;
} T;

/*@ requires \valid(C)
  @ assigns C->O0
  @ ensures C->O0 == (C->I1 && C->I0)
  @*/
void ComputeCommands (T *C){
C->O0 = (C->I1) && (C->I0);
}

Here, I get an error message when I compile with Caduceus:

$ caduceus ComputeCommands_essais3.c
File "ComputeCommands_essais3.c", line 9, characters 22-36:
Error: predicates are not allowed here

(line 9 corresponds to the line with ensures). I then looked at the grammar
of Caduceus; for me the term "C->O0 == (C->I1 && C->I0)" should be a
<predicate> as specified on page 25 of the Caduceus reference manual,
therefore the term "(C->I1 && C->I0)" should be a <term>, "==" being a
<relation>; this would require "&&" to be a valid <arith_op>, which is not
the case (the only arith_op allowed being +, -, *, /, %). Is it normal that
we cannot use && as an arithmetic operator, and how would you prove my (very
simple) code?

Thank you for your help,

Jean-Baptiste Jeannin
Hispano-Suiza
jean-baptiste.jeannin@hispano-suiza-sa.com
# " This e-mail and any attached documents may contain confidential or
proprietary information. If you are not the intended recipient, please
advise the sender immediately and delete this e-mail and all attached
documents from your computer system. Any unauthorised disclosure,
distribution or copying hereof is prohibited." " Ce courriel et les
documents qui y sont attaches peuvent contenir des informations
confidentielles. Si vous n'etes pas le destinataire escompte, merci d'en
informer l'expediteur immediatement et de detruire ce courriel ainsi que
tous les documents attaches de votre systeme informatique. Toute
divulgation, distribution ou copie du present courriel et des documents
attaches sans autorisation prealable de son emetteur est interdite." #
_______________________________________________
Why-discuss mailing list
Why-discuss@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why-discuss




-- 
Yannick
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20080804/6c97d74c/attachment.htm