--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on June 2019 ---
[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>