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] why-2.24 install question
- Subject: [Frama-c-discuss] why-2.24 install question
- From: virgile.prevosto at cea.fr (Virgile Prevosto)
- Date: Wed, 21 Apr 2010 11:24:42 +0200
- In-reply-to: <20100421085841.GA17441@opentech.at>
- References: <4BCD7302.4010608@cea.fr> <20100420092826.GA18012@opentech.at> <4BCD74FB.5@inria.fr> <20100420094716.GA29920@opentech.at> <k2wb15d09071004200309s9b16d74blf291bb5311524916@mail.gmail.com> <20100420101921.GA20284@opentech.at> <20100420140021.6877f00a@is010235> <20100420165535.GA25683@opentech.at> <4BCEAB16.8030702@inria.fr> <4BCEB130.9040205@inria.fr> <20100421085841.GA17441@opentech.at>
Le mer. 21 avril 2010 10:58:41 CEST, Nicholas Mc Guire <der.herr at hofr.at> a ?crit : > /*@ requires \valid(i) && \valid(j); > @ requires r == NULL || \valid(r); > @ assigns *r; > @ behavior zero: > @ assumes r == NULL; > @ assigns \nothing; > @ ensures \result == -1; > @ behavior normal: > @ assumes \valid(r); > @ assigns *r; > @ ensures *r == ((*i < *j) ? *j : *i); > @ ensures \result == 0; > @*/ > int max(int *r, int* i, int* j) { > if (!r) return -1; > *r = (*i < *j) ? *j : *i; > return 0; > } > > ... > max1.c:2:[kernel] user error: Error during annotations analysis: unbound logic variable NULL > ... > There are 2 points here: NULL is supposed to be a macro, but the jessie tutorial does not include stddef.h, which is supposed to define it. #include "stddef.h" in max1.c should do the trick, together with the option -cpp-extra-args="-I`frama-c -print-path`/libc", to retrieve the header provided by frama-c. Alternatively, -cpp-extra-args="-DNULL=0" should do the trick for this particular case. The second point is what Claude said: C pre-processors do not traverse comment, which is what an annotation is for what cpp is concerned. Normally, you would need to add the option -pp-annot to frama-c's command-line to force the pre-processing of annotation. Note that this can be done only when the pre-processor is cpp/gcc. This is why -pp-annot is not the default. However, If I recall correctly, the Jessie plug-in already sets that automatically for you (without much regard of what your pre-processor looks like, but that's another story). Anyway, using the \null built-in of ACSL is definitely the recommended way. Hope this helps, -- E tutto per oggi, a la prossima volta. Virgile
- Follow-Ups:
- [Frama-c-discuss] why-2.24 install question
- From: der.herr at hofr.at (Nicholas Mc Guire)
- [Frama-c-discuss] why-2.24 install question
- References:
- [Frama-c-discuss] why-2.24 install question
- From: Julien.Signoles at cea.fr (Julien Signoles)
- [Frama-c-discuss] why-2.24 install question
- From: der.herr at hofr.at (Nicholas Mc Guire)
- [Frama-c-discuss] why-2.24 install question
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] why-2.24 install question
- From: der.herr at hofr.at (Nicholas Mc Guire)
- [Frama-c-discuss] why-2.24 install question
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] why-2.24 install question
- From: der.herr at hofr.at (Nicholas Mc Guire)
- [Frama-c-discuss] why-2.24 install question
- From: virgile.prevosto at cea.fr (Virgile Prevosto)
- [Frama-c-discuss] why-2.24 install question
- From: der.herr at hofr.at (Nicholas Mc Guire)
- [Frama-c-discuss] why-2.24 install question
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] why-2.24 install question
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] why-2.24 install question
- From: der.herr at hofr.at (Nicholas Mc Guire)
- [Frama-c-discuss] why-2.24 install question
- Prev by Date: [Frama-c-discuss] why-2.24 install question
- Next by Date: [Frama-c-discuss] why-2.24 install question
- Previous by thread: [Frama-c-discuss] why-2.24 install question
- Next by thread: [Frama-c-discuss] why-2.24 install question
- Index(es):