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

[no subject]



   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>