Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Enforcing assigns contract with EVA/from plugin?

  • Subject: [Frama-c-discuss] Enforcing assigns contract with EVA/from plugin?
  • From: rod at proteancode.com (Roderick Chapman)
  • Date: Mon, 10 Jun 2019 14:47:04 +0100
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>