--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on July 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Automating proof on data invariant with Wp



Hello,

I'm currently working on a project to verify invariant on data-types 
with relaxed concurrency models: reading are made out of critical 
regions, it's up to the writing thread to maintain the invariant each 
time a data is available to others.

I'm aware there is a way to declare weak and strong invariant, but I 
want to check them at specific instructions.
My typical example is the follow :

```C
struct point {
   int x, y;
};
\\@ on_visible (this.x > this.y);

int main(){
   struct point *pt = malloc(...);
   ...
   //@ make_visible pt;      <- invariant should hold at this point!
   ...
}
```

With the `register_global` function we have a `lexpr_node` that 
represents the invariant. I want to avoid an «ad hoc» translator since 
it may not be generic.
How can we translate it to an assertion that could be checked with Wp?

Best regards,

--
Josselin Giet
M2 DI/ENS