update according to kernel changes (\specified)

src/plugins/e-acsl/pre_analysis.ml

@@ -323,6 +323,7 @@ module rec Transfer
     | Pfreeable _ -> Error.not_yet "\\freeable"
     | Pfresh _ -> Error.not_yet "\\fresh"
     | Pseparated _ -> Error.not_yet "\\separated"
+    | Pspecified _ -> Error.not_yet "\\specified"
     | Ptrue | Pfalse | Papp _ | Prel _
     | Pand _ | Por _ | Pxor _ | Pimplies _ | Piff _ | Pnot _ | Pif _ 
     | Plet _ | Pforall _ | Pexists _ | Pat _ | Psubtype _ ->

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle

@@ -69,7 +69,7 @@ tests/e-acsl-runtime/valid.c:47:[value] Assertion got status valid.
 FRAMAC_SHARE/libc/stdlib.h:175:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
 FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 tests/e-acsl-runtime/valid.c:49:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid.c:49:[kernel] warning: accessing left-value that contains escaping addresses; assert(\defined(&a))
+tests/e-acsl-runtime/valid.c:49:[kernel] warning: accessing left-value that contains escaping addresses: assert \specified(&a);
 tests/e-acsl-runtime/valid.c:49:[kernel] warning: completely indeterminate value in a.
 tests/e-acsl-runtime/valid.c:49:[value] all evaluations are invalid for function call argument
         (void *)a

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle

@@ -61,7 +61,7 @@ tests/e-acsl-runtime/valid.c:47:[value] Assertion got status valid.
 FRAMAC_SHARE/libc/stdlib.h:175:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
 FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 tests/e-acsl-runtime/valid.c:49:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid.c:49:[kernel] warning: accessing left-value that contains escaping addresses; assert(\defined(&a))
+tests/e-acsl-runtime/valid.c:49:[kernel] warning: accessing left-value that contains escaping addresses: assert \specified(&a);
 tests/e-acsl-runtime/valid.c:49:[kernel] warning: completely indeterminate value in a.
 tests/e-acsl-runtime/valid.c:49:[value] all evaluations are invalid for function call argument
         (void *)a

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle

@@ -58,11 +58,11 @@ tests/e-acsl-runtime/valid_alias.c:17:[value] Assertion got status valid.
 FRAMAC_SHARE/libc/stdlib.h:175:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
 FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 tests/e-acsl-runtime/valid_alias.c:19:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses; assert(\defined(&a))
+tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses: assert \specified(&a);
 tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: completely indeterminate value in a.
 tests/e-acsl-runtime/valid_alias.c:19:[value] all evaluations are invalid for function call argument
         (void *)a
-tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses; assert(\defined(&b))
+tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses: assert \specified(&b);
 tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: completely indeterminate value in b.
 tests/e-acsl-runtime/valid_alias.c:19:[value] all evaluations are invalid for function call argument
         (void *)b

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle

@@ -56,11 +56,11 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition
 FRAMAC_SHARE/libc/stdlib.h:175:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
 FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 tests/e-acsl-runtime/valid_alias.c:19:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses; assert(\defined(&a))
+tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses: assert \specified(&a);
 tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: completely indeterminate value in a.
 tests/e-acsl-runtime/valid_alias.c:19:[value] all evaluations are invalid for function call argument
         (void *)a
-tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses; assert(\defined(&b))
+tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses: assert \specified(&b);
 tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: completely indeterminate value in b.
 tests/e-acsl-runtime/valid_alias.c:19:[value] all evaluations are invalid for function call argument
         (void *)b

src/plugins/e-acsl/translate.ml

@@ -531,6 +531,7 @@ and named_predicate_content_to_exp ?name kf env p =
   | Ptrue -> Cil.one ~loc, env
   | Papp _ -> not_yet env "logic function application"
   | Pseparated _ -> not_yet env "\\separated"
+  | Pspecified _ -> not_yet env "\\specified"
   | Prel(rel, t1, t2) -> 
     let e, env = 
       comparison_to_exp ~loc kf env (relation_to_binop rel) t1 t2 None 

src/plugins/e-acsl/typing.ml

@@ -441,6 +441,7 @@ let rec type_predicate_named p =
   | Pfalse | Ptrue -> ()
   | Papp _ -> Error.not_yet "logic function application"
   | Pseparated _ -> Error.not_yet "\\separated"
+  | Pspecified _ -> Error.not_yet "\\specified"
   | Prel(_, t1, t2) -> 
     ignore (type_term t1);
     ignore (type_term t2)