--- layout: fc_discuss_archives title: Message 7 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?



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>