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?

Hello Rod,

I would say the [eva:alarm] is precisely your error, \from part which is not validated.

I don't know if there is a switch to block analysis at that point. In that past, I used some grep scripts to find any alarm in a log file.

Best regards,
David


Le 10 juin 2019 22:47:04 GMT+09:00, Roderick Chapman <rod at proteancode.com> a écrit :
>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;
>}

-- 
Envoyé de mon appareil Android avec Courriel K-9 Mail. Veuillez excuser ma brièveté.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190611/6a28d9be/attachment.html>