From eea8022a7d10fdb86cdb25e6a8b395afa423828e Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 14 Jun 2022 18:31:54 +0200
Subject: [PATCH] [tests] add variation on \ghost result type and assigns test
---
tests/spec/ghost_result_type.i | 6 ++++++
tests/spec/oracle/ghost_result_type.res.oracle | 8 ++++++++
2 files changed, 14 insertions(+)
diff --git a/tests/spec/ghost_result_type.i b/tests/spec/ghost_result_type.i
index 9adaff7cfb2..84ce3ad190c 100644
--- a/tests/spec/ghost_result_type.i
+++ b/tests/spec/ghost_result_type.i
@@ -3,6 +3,12 @@
int *f(void);
*/
+/*@ ghost
+ /@ assigns \result,*\result \from \nothing; @/
+ int \ghost * g(void);
+*/
+
int main(void){
//@ ghost int* p = f() ;
+ //@ ghost int \ghost* q = g() ;
}
diff --git a/tests/spec/oracle/ghost_result_type.res.oracle b/tests/spec/oracle/ghost_result_type.res.oracle
index 9eb79cb2962..0bd50ab54f7 100644
--- a/tests/spec/oracle/ghost_result_type.res.oracle
+++ b/tests/spec/oracle/ghost_result_type.res.oracle
@@ -4,10 +4,18 @@
assigns \result \from \nothing; @/
int *f(void); */
+/*@ ghost
+/@ assigns \result, *\result;
+ assigns \result \from \nothing;
+ assigns *\result \from \nothing;
+ @/
+int \ghost *g(void); */
+
int main(void)
{
int __retres;
/*@ ghost int *p = f(); */
+ /*@ ghost int \ghost *q = g(); */
__retres = 0;
return __retres;
}
--
GitLab