|Anonymous | Login | Signup for a new account||2019-05-22 17:57 CEST|
|Main | My View | View Issues | Change Log | Roadmap | Repositories|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0000615||Frama-C||Plug-in > jessie||public||2010-10-22 18:54||2010-10-22 22:20|
|Product Version||Frama-C Boron-20100401|
|Target Version||Fixed in Version|
|Summary||0000615: separately verified files show code-bug when linked together|
|Description||The 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.
|Tags||No tags attached.|
|Attached Files||ftest_2files [^] (848 bytes) 2010-10-22 18:54 [Show Content]|
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.
|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|