Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000615Frama-CPlug-in > jessiepublic2010-10-22 18:542010-10-22 22:20
ReporterJochen 
Assigned Tocmarche 
PrioritynormalSeveritymajorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in Version 
Summary0000615: separately verified files show code-bug when linked together
DescriptionThe attached file contains the files "ftest3a.c" and "ftestMain.c. Each of them can be verified (by alt-ergo), except for "\valid(&b)" in ftestMain, cf. issue 0000614. Although the "assert res == 1" in ftestMain is verified, it does not hold, as can be seen by removing both "////"-comments, compiling, and running: "gcc ftest3a.c ftestMain.c && ./a.out" yields "main: res=0\n" on stdout. Note that the contracts of "f()" and "g()" are identical across both files, and that they don't omit neccessary or provide invalid preconditions (e.g. no "assigns \nothing"). Also, the "no-regions"-model is used in both files.
The parameter "x" in "g()" is an alias to the global "b", and "f()" modifies "b". Both facts can be detected only by looking into ftestMain. Hence, by looking into ftest3a only, it cannot be detected that "g"s ensures clause is wrong; there is no other hint than nonexistent "assigns"-clauses.
TagsNo tags attached.
Attached Files? file icon ftest_2files [^] (848 bytes) 2010-10-22 18:54 [Show Content]

- Relationships

-  Notes
(0001245)
pascal (reporter)
2010-10-22 22:20

Hello Jochen,

you probably discovered an issue with implicit assigns clauses (am I right? Can you reproduce the problem if you force yourself to write explicit assigns clauses in every function contract?)

But, I would like to point out that it has probably never been guaranteed that you could verify C files separately, then link them together and expect the resulting program to work. There are too many issues with C's link-time "actions", such as, out the top of my head, incomplete types that only become fully known at link time. The Burstall-Bornat model assumes that types are completely known, and is unsound otherwise.

Yet, incomplete types and other potential pitfalls are minor issues. You can verify files that do not make a full program, write invariants and debug specifications in this mode. But you should probably run the verification again on the whole set of files when they are all available. If you did not use incomplete types or other strange C link-time features, the verification should pass again without modifications. But I am afraid that C is too weird for us to be able to offer "modular verification" in the sense of looking separately at each file. We only offer "modular verification" in the sense above where you should run the verification again on the complete program to be safe.

Your bug report does not use incomplete types, though, and is probably a valid bug report regardless of my remark.

- Issue History
Date Modified Username Field Change
2010-10-22 18:54 Jochen New Issue
2010-10-22 18:54 Jochen Status new => assigned
2010-10-22 18:54 Jochen Assigned To => cmarche
2010-10-22 18:54 Jochen File Added: ftest_2files
2010-10-22 22:20 pascal Note Added: 0001245


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker