Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000215Frama-CPlug-in > jessiepublic2009-08-24 16:262009-08-25 16:37
Reporternstouls 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0000215: Mise en hypothèse de la précondition d'une opération appelée
Descriptionbonjour,

Voici donc un petit exemple en pièce jointe.
Si je souhaite le prouver avec Jessie :

     frama-c t2.c -jessie &

J'obtiens 5 OP.
Celles qui m'intéressent sont les 2 OP de post-condition du main. Prenons par exemple la première des deux :

main_ensures_default_po_1

H1: true = true and (0 <= integer_of_int32(i) and integer_of_int32(i) <= 1)
result: int32
H6: (integer_of_int32(i) = 1 -> integer_of_int32(result) = 1) and
    (integer_of_int32(i) = 0 -> integer_of_int32(result) = 0)
tmp: int32
H7: tmp = result
H8: integer_of_int32(tmp) <> 0
result0: int32
H9: integer_of_int32(result0) = 0
__retres: int32
H10: __retres = result0
return: int32
H11: return = __retres
----------------------------------
integer_of_int32(return) = 0


H1 correspond à la pré-condition de main
H6 est issue de l'appel de fonction f(). C'est la conjonction des assumes impliquant les ensures associés
H7 et + correspond au code de la fonction main.

Dans cet exemple, il n'y a pas d'hypothèse H5 décrivant la pré-condition de f(), alors qu'elle devrait être présente.

En l'occurrence, cette pré-condition étant équivalente à H1, tout se prouve. Mais lorsqu'il est nécessaire de faire un preuve difficile pour faire ce lien, il serait intéressant d'avoir ensuite la pré de f en hypothèse.

Merci beaucoup et bonne journée,
Nicolas.
TagsNo tags attached.
Attached Filesc file icon t2.c [^] (312 bytes) 2009-08-24 16:26 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2009-08-24 16:26 nstouls New Issue
2009-08-24 16:26 nstouls File Added: t2.c
2009-08-25 16:37 signoles Status new => assigned
2009-08-25 16:37 signoles Assigned To => cmarche


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker