--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on June 2019 ---
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; } -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190610/40f10d72/attachment.html>