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]

[Frama-c-discuss] Enforcing assigns contract with EVA/from plugin?

1. The message means the plugin was not able to verify the properties, 
but due to incompleteness (overapproximations), it cannot categorically 
state whether this is because the property is indeed false, or due to a 
limitation of the plugin. The "cannot validate direct dependencies" 
means at least one direct dependency was not validated. Same for 
indirect ones. Adding "indirect:x, g" to the assigns clause should solve it.

2. The new warning mechanism (since Frama-C Chlorine), based on 
-*-warn-key (similar to the old -*-msg-key, but for warnings/errors) 
does allow converting warnings of a particular kind into errors, using 
just the command line, but it has not been ported to this warning. In 
particular, the code that uses it is also related to other warnings, so 
it is not obvious whether the transition would be trivial. But with each 
Frama-C release, more of these warnings become configurable, so 
reporting which of them interest you increases the chances that this may 
happen.

So, for now, I'm afraid it's not possible to convert it to an error 
without patching Frama-C.


On 10/06/2019 15:47, Roderick Chapman wrote:
>
> Next question: is it possible to have the EVA/From plug-in report an 
> error when a user-written "assigns" contract does not precisely match 
> the computed dependency relation?
>
> For example, in the code below, the "assigns" contract and the code do 
> not match.
>
> If I use -from-verify-assigns, then I get
>
> [eva:alarm] try.c:5: Warning:
>   function try: \from ... part in assign clause got status unknown 
> (cannot validate direct and indirect dependencies).
> [eva] done for function try
> [from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
> [from] entry point:
>   \result FROM x; g
> [from] ====== END OF CALLWISE DEPENDENCIES ======
>
> But...
>
> 1. What does the first warning really mean? Why can't it validate the 
> dependencies?
>
> 2. The reported computed dependency is correct and doesn't match the 
> assigns contract. Can I get it to report an error in this case?
>
>  Thanks,
>
>  Rod
>
> --- cut ---
>
> static int g = 5;
>
> /*@ requires x == 20;
>     assigns \result \from x; // wrong - should be x, g;
>  */
> int try (int x)
> {
>   int t = 0;
>   int t2;
>   if (x > 10)
>     t = g + 1; // here is ref to g
>   t2 = x - t;
>
>   return t2;
> }
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-- 
André Maroneze
Researcher/Engineer CEA/List
Software Reliability and Security Laboratory

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190611/d449748b/attachment.html>