Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] wp calculus

On Mon, Jun 22, 2009 at 11:45 AM, Anne
Pacalet<anne.pacalet at sophia.inria.fr> wrote:
> I cannot answer about WHY, but because I am developing a new WP plugin
> for Frama-C, I am very interested by your question.
> What kind of commands would you need ?
> Is it to interact with another tool ?

I'm develping a tool for automatic generation of test suites
the approach uses wp calculus to refine a model of the state space of
the program under test (I can give more details if needed)
the tool uses CIL and I would like to use an existing wp calculator
compartible with it

what I need is to obtain the precondition that guarantees that the
execution of a given C statement brings the program in a state
fullfilling a given C (if possible) predicate... ex:

WP(x = x+1, x < 1) =(x<0)

the algorithms works on single paths so there is no need to calculate
wp for loops...
I would instead need to be able to calculate wp for assume statements
and sequences of statements

In my dreams this would be given by an API usable directly in C...

pleas ask for any further clarification

thank you
Mauro
-- 
Computer science is no more about computers than astronomy is about telescopes
    - Edsger W. Dijkstra