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] Re: questions about FRAMA-C

  • Subject: [Frama-c-discuss] Re: questions about FRAMA-C
  • From: ioana-mihaela.geanta at atosorigin.com (IOANA MIHAELA GEANTA)
  • Date: Wed Oct 29 16:58:24 2008
I'm sorry for the attachments, I will enclose them in this message.

I hope you can take a look at the examples, especially at the one concerning structures.

Thank you,
Ioana Geanta

Hello,
Le mer 29 oct 2008 15:18:31 CET,
IOANA MIHAELA GEANTA <ioana-mihaela.geanta at atosorigin.com> a ?crit :

> 1.Assignment of structures:  For pointers to structures, how does the assigns clause has to be used : assigns p or assigns *p?

assigns *p;

'assigns p;' would mean that the pointer itself might be modified.
 
>   In the second case I get the next error :
>   Fatal error: exception Assert_failure("src/jessie/interp.ml", 531, 15).
>  
>   I made an example which illustrates this case : cas_structure.tar.gz
> 
> 
> 2. Values of enum types are not accepted in predicates  (cas_constante.tar.gz).
> 

Apparently the code examples have been lost somewhere, so that it is
difficult to address your issue precisely. The following code:

//@ assigns *p;
void bar(int *p);

enum foo { FOO, BAR };

//@ predicate is_FOO(enum foo x) = x == FOO;

int main() {
  enum foo x = BAR;
  //@assert !is_Foo(x);
  int y;
  bar(&y);
  return 0;
}


is handled correctly by Frama-C Helium.

> 3. "\let" clauses are not implemented in FRAMA-C which makes difficult verifying functions which have references as parameters. The values pointed by these references are difficult to use in the annotations, for example in predicates for properties of functions which call the first function.
>     The only possibility is to use ghost variables. The problem is that the formal specification should be written  before coding, so ghosts variables cannot be defined at this point.   
>   Do you this this feature will be implemented in the future ?
> 
> 4. In a defined behavior, it is not possible to use a requires clause after the assume clause that defines the behavior. I took an example from the ACSL implementation, included in the distribution of FRAMA-C and I got a syntax error.
> 

All ACSL constructions are meant to be supported by Frama-C at some
point (but I can't be more precise than that, except that \let and
requires in behavior won't be present in the next release). The current
state of the implementation is described in acsl-implementation.pdf in
the doc/ directory of the sources. Note however that implementation here
only means that the annotation is type-checked by Frama-C kernel. The
analysis plugins themselves may have further limitations, which are
normally listed in each plugin's documentation.

Best regards,
-- 
E tutto per oggi, a la prossima volta.
Virgile Prevosto


-------------- section suivante --------------
Une pi?ce jointe non texte a ?t? nettoy?e...
Nom: cas_constante.tar.gz
Type: application/x-gzip
Taille: 1351 octets
Desc: non disponible
Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081029/f15a3a54/cas_constante.tar-0001.bin
-------------- section suivante --------------
Une pi?ce jointe non texte a ?t? nettoy?e...
Nom: cas_structure.tar.gz
Type: application/x-gzip
Taille: 1060 octets
Desc: non disponible
Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081029/f15a3a54/cas_structure.tar-0001.bin