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]

[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>