diff --git a/tests/spec/assignable_location.i b/tests/spec/assignable_location.i index f7165642c352a6b605e3a3bc682e338dad40c2a0..70968c3735ad313c5896d7125e9f350e4c4a509d 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 f366f6bd4c096c5f60a1dc7f61be904f58497e50..775b7573457de6e89e8f89b34a7728b717a216c2 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