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