From dda13ade2182e6573520127b1966275ae1a6a6f0 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 29 Sep 2020 12:44:53 +0200
Subject: [PATCH] [kernel] Tests \from address
---
tests/spec/assignable_location.i | 16 +++++++++++-
.../oracle/assignable_location.res.oracle | 26 +++++++++++--------
2 files changed, 30 insertions(+), 12 deletions(-)
diff --git a/tests/spec/assignable_location.i b/tests/spec/assignable_location.i
index f7165642c35..70968c3735a 100644
--- a/tests/spec/assignable_location.i
+++ b/tests/spec/assignable_location.i
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config
OPT: -kernel-warn-key=annot-error=active
*/
@@ -18,6 +18,13 @@ double annotations_to_accept(typetab *t) {
return f(t);
}
+/*@ behavior acc_0: assigns \result \from &x ;
+ behavior acc_1: assigns \result \from &f ;
+*/
+int * from_address_to_accept(int f){
+ return (void*)0 ;
+}
+
int g(void);
@@ -39,3 +46,10 @@ int annotations_to_reject(void) {
//@ behavior to_reject_6: assigns x \from lx;
return g();
}
+
+/*@ behavior rej_0: assigns \result \from &l ; */
+int * from_address_to_reject(int f){
+ int l ;
+ //@ behavior rej_1: assigns l \from &lx ;
+ return (void*)0 ;
+}
diff --git a/tests/spec/oracle/assignable_location.res.oracle b/tests/spec/oracle/assignable_location.res.oracle
index f366f6bd4c0..775b7573457 100644
--- a/tests/spec/oracle/assignable_location.res.oracle
+++ b/tests/spec/oracle/assignable_location.res.oracle
@@ -1,23 +1,27 @@
[kernel] Parsing tests/spec/assignable_location.i (no preprocessing)
-[kernel:annot-error] tests/spec/assignable_location.i:36: Warning:
+[kernel:annot-error] tests/spec/assignable_location.i:43: Warning:
unexpected token ';'
-[kernel:annot-error] tests/spec/assignable_location.i:28: Warning:
+[kernel:annot-error] tests/spec/assignable_location.i:35: Warning:
not an addressable left value: \result. Ignoring logic specification of function annotations_to_reject
-[kernel:annot-error] tests/spec/assignable_location.i:30: Warning:
+[kernel:annot-error] tests/spec/assignable_location.i:37: Warning:
not an assignable left value: *t. Ignoring code annotation
-[kernel:annot-error] tests/spec/assignable_location.i:31: Warning:
+[kernel:annot-error] tests/spec/assignable_location.i:38: Warning:
not an assignable left value: *(t + 0). Ignoring code annotation
-[kernel:annot-error] tests/spec/assignable_location.i:32: Warning:
+[kernel:annot-error] tests/spec/assignable_location.i:39: Warning:
not an assignable left value: *(t + (0 .. 0)). Ignoring code annotation
-[kernel:annot-error] tests/spec/assignable_location.i:33: Warning:
+[kernel:annot-error] tests/spec/assignable_location.i:40: Warning:
not an assignable left value: (int)x. Ignoring code annotation
-[kernel:annot-error] tests/spec/assignable_location.i:34: Warning:
+[kernel:annot-error] tests/spec/assignable_location.i:41: Warning:
not an assignable left value: (char)x. Ignoring code annotation
-[kernel:annot-error] tests/spec/assignable_location.i:35: Warning:
+[kernel:annot-error] tests/spec/assignable_location.i:42: Warning:
not an addressable left value: (char)x. Ignoring code annotation
-[kernel:annot-error] tests/spec/assignable_location.i:37: Warning:
+[kernel:annot-error] tests/spec/assignable_location.i:44: Warning:
not an addressable left value: \empty. Ignoring code annotation
-[kernel:annot-error] tests/spec/assignable_location.i:38: Warning:
+[kernel:annot-error] tests/spec/assignable_location.i:45: Warning:
not an assignable left value: lx. Ignoring code annotation
-[kernel:annot-error] tests/spec/assignable_location.i:39: Warning:
+[kernel:annot-error] tests/spec/assignable_location.i:46: Warning:
not a valid dependency: lx. Ignoring code annotation
+[kernel:annot-error] tests/spec/assignable_location.i:50: Warning:
+ unbound logic variable l. Ignoring logic specification of function from_address_to_reject
+[kernel:annot-error] tests/spec/assignable_location.i:53: Warning:
+ not an addressable left value: lx. Ignoring code annotation
--
GitLab