--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on October 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Incremental verification



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