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] question about axiomatic and type invariant

  • Subject: [Frama-c-discuss] question about axiomatic and type invariant
  • From: wfordlon at dso.org.sg (Wong Ford Long)
  • Date: Fri, 30 Jan 2015 08:58:38 +0000
Dear All,

I analyzed the C source code from the ACSL-Tutorial document
 (http://frama-c.com/download/acsl-tutorial.pdf),
 namely parts of chapters 8 and 9.
Let's call the source code below function2.c

The Neon version of Frama-C is used, with the command
> frama-c-gui -wp -wp-rte function2.c

_________________________________________________________________

typedef struct _list { int element; struct _list* next; } list;

/*@
inductive reachable{L} (list* root, list* node) {
  case root_reachable{L}:
       \forall list* root; reachable(root,root);
  case next_reachable{L}:
       \forall list* root, *node;
       \valid(root) ==> reachable(root->next, node) ==>
       reachable(root,node);
}
*/

/*@ predicate finite{L}(list* root) = reachable(root,\null); */

/*@ type invariant finite_list(list* root) = finite(root); */

/*@ axiomatic Length {
  logic integer length{L}(list* l);
  axiom length_nil{L}: length(\null) == 0;
  axiom length_cons{L}:
      \forall list* l, integer n;
         finite(l) && \valid(l) ==>
           length(l) == length(l->next) + 1;
  }
*/


/*@
    requires \valid(root);
    assigns \nothing;
    ensures
     \forall list* l;
       \valid(l) && reachable(root,l) ==>
         \result >= l->element;
    ensures
     \exists list* l;
       \valid(l) && reachable(root,l) && \result == l->element;
*/
int max_list(list* root) {
  int max = root->element;
  while(root->next) {
    root = root-> next;
    if (root->element > max) max = root->element;
  }
  return max;
}

________________________________________________________________

The console output is as follows:


[kernel] preprocessing with "gcc -C -E -I.  function2.c"
[kernel] warning: ignoring status of type invariant `finite_list'
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
function2.c:17:[wp] warning: Type invariant not handled yet ('finite_list' ignored)
[rte] annotating function max_list
[wp] warning: No definition for 'length' interpreted as reads nothing
function2.c:43:[wp] warning: Missing assigns clause (assigns 'everything' instead)
[wp] 9 goals scheduled
[wp] [Alt-Ergo] Goal typed_max_list_assert_rte_mem_access : Valid (25ms) (12)
[wp] [Alt-Ergo] Goal typed_max_list_assert_rte_mem_access_2 : Unknown
[wp] [Alt-Ergo] Goal typed_max_list_post_2 : Unknown (Qed:1ms)
[wp] [Qed] Goal typed_max_list_assert_rte_mem_access_3 : Valid
[wp] [Qed] Goal typed_max_list_assert_rte_mem_access_5 : Valid (1ms)
[wp] [Qed] Goal typed_max_list_assign_part1 : Valid
[wp] [Alt-Ergo] Goal typed_max_list_post : Unknown (1s)
[wp] [Alt-Ergo] Goal typed_max_list_assert_rte_mem_access_4 : Unknown (1s)
[wp] [Alt-Ergo] Goal typed_max_list_assign_part2 : Unknown
[wp] Proved goals:    4 / 9
     Qed:             3  (0ms-1ms)
     Alt-Ergo:        1  (25ms-25ms) (12) (unknown: 5)


________________________________________________________________

Regarding
[wp] warning: No definition for 'length' interpreted as reads nothing

How should this message be understood?
Has something above been written wrongly, causing 'length' to be undefined?
How to correct this, so that 'length' can be used in the annotation
of some function that manipulates the struct 'list'?


Regarding
function2.c:17:[wp] warning: Type invariant not handled yet ('finite_list' ignored)

Does the Neon version (ver 20140301) of Frama-C handle such type invariant?
Or would future versions do so?


 Thanks and best regards,
 Ford

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150130/70e81e8e/attachment-0001.html>