--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on October 2010 ---
On Wed, 2010-10-06 at 16:58 +0200, Virgile Prevosto wrote: > The parser itself has absolutely no way to know what has changed unless > you give it the two versions of the code. And even in this case, the > diff won't be that easy. In my opinion, the best way to handle that is > within your favorite IDE (Eclipse, Emacs, Vim, ...), since it knows > exactly which changes have been made. Chances are that it has already > some notions of C, and as Pascal said, a rudimentary ACSL parser > should be sufficient at this level. In this case, what does a parser have to do and how must it interact with Frama-C/Jessie? For example: - if I change void foo() { int i; i = 0; } to void foo() { int i; j = 0; } does the parser have to detect that j is undeclared? - if I change the contract of a function f that is used by several other functions, does the parser have to detect which functions depend on f and have Jessie verify each of them again, or is it sufficient to notify Jessie of this change and Jessie will verify f along with its callers? -- Regards, Boris