--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on July 2020 ---
struct point { ⦠}; //@ predicate visible{L}(struct point * this) = ⦠; int main() { struct point * pt = ⦠; ... //@ assert visible(pt); ⦠} Although, if you want to systematically insert assertions in some places, you will have to use dedicated Frama-C plugin for that. You can actually define new ACSL annotations and use them to populate the Frama-C AST with new assertions, that will be handled by any other plugins afterwards. Regards, L. > Le 7 juil. 2020 à 07:52, Josselin Giet <josselin.giet at ens.fr> a écrit : > > 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 > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200707/93af9b04/attachment.html>