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] Probleme lancement

  • Subject: [Frama-c-discuss] Probleme lancement
  • From: nicolas.muller at sagem.com (MULLER Nicolas (SAGEM DEFENSE SECURITE))
  • Date: Mon, 4 Oct 2010 10:29:01 +0200
Suite au probl?me d?j? mentionn? dans le mail  ?PB in FramaC installation ? (le 24/09/2010), nous avons ?tablit qu'il s'agit tr?s probablement d'un probl?me d'installation, plus particuli?rement d'incompatibilit? avec notre configuration  syst?me windows XP SP3


Rappel des sympt?mes :

La commande
frama-c -jessie -jessie-atp alt-ergo test3.c (test3.c ?tant un fichier quelconque)
proc?de bien au parsing du fichier, mais retourne syst?matiquement des failures.
(voir d?tails dans le fichier joint)

Proc?dure d'investigation suivie :
apr?s avoir constat? l'occurrence syst?matique de ? failures ? (ind?cision du prover) sur l'ihm jessie et ce pour tous les provers et quelque soit le fichier pris en compte, nous avons lanc? individuellement des prover en commande ligne.

Le r?sultat est syst?matiquement celui indiqu? dans le listing ci-joint.
[kernel] preprocessing with "gcc -C -E -I.  -dD C:\Documents and Settings\g214950.SAGEM\Bureau\nmuller\R&T\U3CAT\framaC\examples\test3.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir C:\Documents and Settings\g214950.SAGEM\Bureau\nmuller\R&T\U3CAT\framaC\examples\test3.jessie
[jessie] File C:\Documents and Settings\g214950.SAGEM\Bureau\nmuller\R&T\U3CAT\framaC\examples\test3.jessie/test3.jc written.
[jessie] File C:\Documents and Settings\g214950.SAGEM\Bureau\nmuller\R&T\U3CAT\framaC\examples\test3.jessie/test3.cloc written.
[jessie] Calling Jessie tool in subdir C:\Documents and Settings\g214950.SAGEM\Bureau\nmuller\R&T\U3CAT\framaC\examples\test3.jessie
Generating Why function max_ptr
[jessie] Calling VCs generator.
why -alt-ergo [...] why/test3.why
Running Alt-Ergo on proof obligations
(. = valid * = invalid ? = unknown # = timeout ! = failure)
why/test3_why.why             : !!!! (0/0/0/0/4)
total   :   4
valid   :   0 (  0%)
invalid :   0 (  0%)
unknown :   0 (  0%)
timeout :   0 (  0%)
failure :   4 (100%)
total wallclock time : 0.20 sec
total CPU time       : 0.17 sec
valid VCs:
    average CPU time : -1.#J
    max CPU time     : 0.00
invalid VCs:
    average CPU time : -1.#J
    max CPU time     : 0.00
unknown VCs:
    average CPU time : -1.#J
    max CPU time     : 0.00

La trace obtenue en mode debug est disponible sur demande.
il en est de meme pour les fichiers temporaires de trace g?n?r?s en mode debug.

Les variables d'environnements et les paths ont ?t? v?rifi?s.
Le contenu des directories de frama-C ont ?t? v?rifi?s : pas de probl?me apparent.
Les versions de gcc, de make et de jessie ont ?t? compar? avec l'environnement de Dassault.
Le setup avait ?t? fait (sans report d'erreur particulier) au moyen de l'executable frama-c-Boron-20100401.exe.

L'enchainement des commandes a ?t? le suivant :

>why-config
Alt-ergo, simplify,  Z3 , yices, cvc3  install?s

> frama-c
r?sultat ok
> frama-c -val test3.c
r?sultat ok
>frama-c -jessie
r?sultat ok
> frama-c -jessie -jessie-atp alt-ergo test3.c
-> voir le contenu de la trace obtenue dans le fichier joint.

>why-cpulimit
popup indiquant que le point d'entr?e de la proc?dure cygwin_create_path dans cygwin1.dll est erron?
[cid:image001.jpg at 01CB63AE.F65CFE60]

Restauration de cygwin11.dll ? partir du web:
On n'a plus le message d'erreur, mais le lancement de tout prover donne le m?me r?sultat.

Ces derni?res investigations ont ?t? men?es avec l'aide de Dillon Pariente (Dassault Aviation) qui a eu l'amabilit? de nous aider ? cerner la cause de notre probl?me et que nous remercions vivement pour ses conseils.

Merci par avance de bien vouloir nous aider ? rendre notre configuration op?rationnelle rapidement. Nous sommes tout ? fait dispos? ? nous d?placer dans les ?quipes en charge des livraisons de Frama-C avec notre machine ou ? vous accueillir dans nos locaux (? Massy)

Cordialement,

Nicolas Muller et Philippe Baufreton
Sagem
Safran Electronics Division
100, rue de Paris (Fran?ois Hussenot)
91344 Massy cedex
LEM / PROD
Outils Logiciels
T? 01 58 11 21 37

#
" Ce courriel et les documents qui lui sont joints peuvent contenir des informations confidentielles ou ayant un caract?re priv?. S'ils ne vous sont pas destin?s, nous vous signalons qu'il est strictement interdit de les divulguer, de les reproduire ou d'en utiliser de quelque mani?re que ce soit le contenu. Si ce message vous a ?t? transmis par erreur, merci d'en informer l'exp?diteur et de supprimer imm?diatement de votre syst?me informatique ce courriel ainsi que tous les documents qui y sont attach?s."
******
" This e-mail and any attached documents may contain confidential or proprietary information. If you are not the intended recipient, you are notified that any dissemination, copying of this e-mail and any attachments thereto or use of their contents by any means whatsoever is strictly prohibited. If you have received this e-mail in error, please advise the sender immediately and delete this e-mail and all attached documents from your computer system."
#
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20101004/a1ab6cf8/attachment-0001.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: image001.jpg
Type: image/jpeg
Size: 9727 bytes
Desc: image001.jpg
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20101004/a1ab6cf8/attachment-0001.jpg>