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