--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on July 2020 ---
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