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