us elatest frama-c version

OCamlPro · Aug 13, 2024 · 10adf7d · 10adf7d
1 parent 0abd5aa
commit 10adf7d
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 8 deletions.
diff --git a/dune-project b/dune-project
@@ -63,7 +63,7 @@
    (and
     :with-test
     (>= 2.1)))
-  (frama-c :with-test)
+  (frama-c (and (>= 29.0) :with-test))
   ;; dev
   (bisect_ppx
    (and

diff --git a/owi.opam b/owi.opam
@@ -35,7 +35,7 @@ depends: [
   "processor" {>= "0.2"}
   "odoc" {with-doc}
   "mdx" {with-test & >= "2.1"}
-  "frama-c" {with-test}
+  "frama-c" {>= "29.0" & with-test}
   "bisect_ppx" {>= "2.5" & with-dev-setup}
   "ocb" {>= "0.1" & with-dev-setup}
   "crunch" {with-dev-setup}

diff --git a/test/c/eacsl/not-yet-supported/ghost_struct_field/field.t b/test/c/eacsl/not-yet-supported/ghost_struct_field/field.t
@@ -2,14 +2,18 @@
   [kernel] field.c:9: User Error: 
     redefinition of 'List' in the same scope.
     Previous declaration was at field.c:5
-  [kernel] field.c:13: User Error: 
+  [kernel] field.c:17: User Error: 
     Cannot find field order in type struct List
-    11    }; */
-    12    
-    13    void traverse(struct List* node) /*@ ghost (int length) */ {
-          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-    14        /*@ loop invariant length == node->order;
     15            loop variant length;
+    16        */
+
+    17        while (node != NULL) {
+    18            node = node->next;
+    19            //@ ghost length --;
+    20        }
+
+    21    }
+    22
   [kernel] Frama-C aborted: invalid user input.
   Frama-C failed: run with --debug to get the full error message
   [26]