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] Logical annotations

Thank you all for this answer.
--
Thomas 

-----Message d'origine-----
De : frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] De la part de Claude March?
Envoy? : jeudi 7 mai 2009 12:41
? : Frama-C public discussion
Objet : Re: [Frama-c-discuss] Logical annotations


\sum is not supported (yet...) by jessie plugin, see

http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-March/000985.html

for a discussion about a possible workaround (for \prod, but easily 
adpatable to \sum)

- Claude

PAREAUD, Thomas wrote:
> Dear all,
> 
> Do the "logical annotations" supported by Frama-C/Jessie?
> 
> Running frama-c/jessie on one example of the ACSL reference manual
> (removing double/int conversion issue - see below) I obtained errors.
> 
> Each time I tried to write "\sum" annotations, I obtain errors such as
> "ignoring logic specification of function XXX" or other errors.
> 
> Do you have any idea about the reasons of such errors?
> 
> Can you provide me an example of \sum annotation that works.
> 
> Thank you,
> --
> Thomas Pareaud
> 
> /////////// C FILE //////////////
> /*@ requires n >= 0 && \valid (t+(0..n-1)) ;
>   @ ensures \result == \sum(0,n -1, \lambda integer k; t[k]);
>   @*/
> 
> int  array_sum (int t[], int n) {
>   int i;
>   int  s = 0;
>   /*@ loop invariant 0 <= i <= n;
>     @ loop invariant s == \sum(0, i-1, \lambda integer k; t[k]);
>     @ loop variant n-i;
>     @*/
>   for (i=0; i<n; i++) s += t[i];
>   return s;
> }
> 
> ////////// ERRORS ////////////
> Parsing
> [preprocessing] running gcc -C -E -I. -include
> /usr/local/share/frama-c/jessie/jessie_prolog.h -dD test.c
> Cleaning unused parts
> Symbolic link
> Starting semantical analysis
> Starting Jessie translation
> Fatal error: exception Assert_failure("src/jessie/interp.ml", 564, 19)
> 
> Ce courriel (incluant ses eventuelles pieces jointes) peut contenir des informations confidentielles et/ou protegees ou dont la diffusion est restreinte. Si vous avez recu ce courriel par erreur, vous ne devez ni le copier, ni l'utiliser, ni en divulguer le contenu a quiconque. Merci d'en avertir immediatement l'expediteur et d'effacer ce courriel de votre systeme. Astrium decline toute responsabilite en cas de corruption par virus, d'alteration ou de falsification de ce courriel lors de sa transmission par voie electronique.
> This email (including any attachments) may contain confidential and/or privileged information or information otherwise protected from disclosure. If you are not the intended recipient, please notify the sender immediately, do not copy this message or any attachments and do not use it for any purpose or disclose its content to any person, but delete this message and any attachments from your system. Astrium disclaims any and all liability if this email transmission was virus corrupted, altered or falsified. 
> ---------------------------------------------------------------------
> Astrium SAS (393 341 516 RCS Paris) - Siege social: 6 rue Laurent Pichat, 75016 Paris, France
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |







_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

Ce courriel (incluant ses eventuelles pieces jointes) peut contenir des informations confidentielles et/ou protegees ou dont la diffusion est restreinte. Si vous avez recu ce courriel par erreur, vous ne devez ni le copier, ni l'utiliser, ni en divulguer le contenu a quiconque. Merci d'en avertir immediatement l'expediteur et d'effacer ce courriel de votre systeme. Astrium decline toute responsabilite en cas de corruption par virus, d'alteration ou de falsification de ce courriel lors de sa transmission par voie electronique.
This email (including any attachments) may contain confidential and/or privileged information or information otherwise protected from disclosure. If you are not the intended recipient, please notify the sender immediately, do not copy this message or any attachments and do not use it for any purpose or disclose its content to any person, but delete this message and any attachments from your system. Astrium disclaims any and all liability if this email transmission was virus corrupted, altered or falsified. 
---------------------------------------------------------------------
Astrium SAS (393 341 516 RCS Paris) - Siege social: 6 rue Laurent Pichat, 75016 Paris, France