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>
- Follow-Ups:
- [Frama-c-discuss] Enforcing assigns contract with EVA/from plugin?
- From: david.mentre at bentobako.org (David MENTRE)
- [Frama-c-discuss] Enforcing assigns contract with EVA/from plugin?
- From: Andre.MARONEZE at cea.fr (Andre Maroneze)
- [Frama-c-discuss] Enforcing assigns contract with EVA/from plugin?
- Prev by Date: [Frama-c-discuss] Question on new -eva-precision option in 19
- Next by Date: [Frama-c-discuss] Enforcing assigns contract with EVA/from plugin?
- Previous by thread: [Frama-c-discuss] Question on new -eva-precision option in 19
- Next by thread: [Frama-c-discuss] Enforcing assigns contract with EVA/from plugin?
- Index(es):