From c1e2d8da982fc2e554ead358444c351c5ad31193 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 28 Aug 2019 08:39:04 +0200
Subject: [PATCH] [Kernel] Ensures that infer_annotations assigns \result for
ghost functions
---
.../typing/infer_annotations.ml | 5 +-
tests/spec/assigns_from_kf.i | 22 +++++-
tests/spec/oracle/assigns_from_kf.res.oracle | 68 ++++++++++++++++---
3 files changed, 83 insertions(+), 12 deletions(-)
diff --git a/src/kernel_internals/typing/infer_annotations.ml b/src/kernel_internals/typing/infer_annotations.ml
index 2bc549d5caf..f6e46efb0ca 100644
--- a/src/kernel_internals/typing/infer_annotations.ml
+++ b/src/kernel_internals/typing/infer_annotations.ml
@@ -142,9 +142,10 @@ let assigns_from_prototype kf =
(fun (g, t) acc -> if g then acc else t :: acc) inputs []
in
let inputs = List.map (fun (_g, t) -> t) inputs in
+ let inputs g = if g then inputs else inputs_no_ghost in
let arguments =
List.map
- (fun (g, content) -> content, From (if g then inputs else inputs_no_ghost))
+ (fun (g, content) -> content, From (inputs g))
to_assign
in
match rtyp with
@@ -155,7 +156,7 @@ let assigns_from_prototype kf =
(* assigns result from basic args and content of pointer args *)
let loc = vi.vdecl in
let result = Logic_const.(new_identified_term (tresult ~loc rtyp)) in
- (result, From inputs_no_ghost):: arguments
+ (result, From (inputs vi.vghost)):: arguments
let is_frama_c_builtin name =
Ast_info.is_frama_c_builtin name
diff --git a/tests/spec/assigns_from_kf.i b/tests/spec/assigns_from_kf.i
index cf8f4228ed4..1def9b69986 100644
--- a/tests/spec/assigns_from_kf.i
+++ b/tests/spec/assigns_from_kf.i
@@ -12,8 +12,17 @@ void something_ghost(void) /*@ ghost (int* p) */;
int something_non_ghost_r(int *p);
int something_ghost_r(void) /*@ ghost (int* p) */;
-void both(int* p, int x) /*@ ghost (int* gp, int gx) */;
-int both_r(int* p, int x) /*@ ghost (int* gp, int gx) */;
+void both(int *p, int x) /*@ ghost (int* gp, int gx) */;
+int both_r(int *p, int x) /*@ ghost (int* gp, int gx) */;
+
+/*@ ghost
+ void g_nothing(void);
+ int g_nothing_r(void);
+ void g_something_non_ghost(int *p);
+ int g_something_non_ghost_r(int *p);
+ void g_both(int *p, int x, int *gp, int gx);
+ int g_both_r(int *p, int x, int *gp, int gx);
+*/
void reference(void) {
nothing();
@@ -24,4 +33,13 @@ void reference(void) {
something_ghost_r() /*@ ghost (0) */;
both(0, 1) /*@ ghost (0, 2) */;
both_r(0, 1) /*@ ghost (0, 2) */;
+
+ /*@ ghost
+ g_nothing();
+ g_nothing_r();
+ g_something_non_ghost(0);
+ g_something_non_ghost_r(0);
+ g_both(0, 1, 0, 2);
+ g_both_r(0, 1, 0, 2);
+ */
}
\ No newline at end of file
diff --git a/tests/spec/oracle/assigns_from_kf.res.oracle b/tests/spec/oracle/assigns_from_kf.res.oracle
index ac10b7070c2..1f02fd47e90 100644
--- a/tests/spec/oracle/assigns_from_kf.res.oracle
+++ b/tests/spec/oracle/assigns_from_kf.res.oracle
@@ -1,19 +1,31 @@
[kernel] Parsing tests/spec/assigns_from_kf.i (no preprocessing)
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning:
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning:
Neither code nor specification for function both, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning:
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning:
Neither code nor specification for function both_r, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning:
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning:
+ Neither code nor specification for function g_both, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning:
+ Neither code nor specification for function g_both_r, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning:
+ Neither code nor specification for function g_nothing, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning:
+ Neither code nor specification for function g_nothing_r, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning:
+ Neither code nor specification for function g_something_non_ghost, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning:
+ Neither code nor specification for function g_something_non_ghost_r, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning:
Neither code nor specification for function nothing, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning:
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning:
Neither code nor specification for function nothing_r, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning:
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning:
Neither code nor specification for function something_ghost, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning:
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning:
Neither code nor specification for function something_ghost_r, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning:
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning:
Neither code nor specification for function something_non_ghost, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning:
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning:
Neither code nor specification for function something_non_ghost_r, generating default assigns from the prototype
/* Generated by Frama-C */
/*@ assigns \nothing; */
@@ -55,6 +67,40 @@ void both(int *p, int x) /*@ ghost (int *gp, int gx) */;
*/
int both_r(int *p, int x) /*@ ghost (int *gp, int gx) */;
+/*@ ghost /@ assigns \nothing; @/
+void g_nothing(void); */
+
+/*@ ghost
+/@ assigns \result;
+ assigns \result \from \nothing; @/
+int g_nothing_r(void); */
+
+/*@ ghost
+/@ assigns *p;
+ assigns *p \from *p; @/
+void g_something_non_ghost(int *p); */
+
+/*@ ghost
+/@ assigns \result, *p;
+ assigns \result \from *p;
+ assigns *p \from *p; @/
+int g_something_non_ghost_r(int *p); */
+
+/*@ ghost
+/@ assigns *p, *gp;
+ assigns *p \from *p, *gp, x, gx;
+ assigns *gp \from *p, *gp, x, gx;
+ @/
+void g_both(int *p, int x, int *gp, int gx); */
+
+/*@ ghost
+/@ assigns \result, *p, *gp;
+ assigns \result \from *p, *gp, x, gx;
+ assigns *p \from *p, *gp, x, gx;
+ assigns *gp \from *p, *gp, x, gx;
+ @/
+int g_both_r(int *p, int x, int *gp, int gx); */
+
void reference(void)
{
nothing();
@@ -65,6 +111,12 @@ void reference(void)
something_ghost_r() /*@ ghost ((int *)0) */;
both((int *)0,1) /*@ ghost ((int *)0,2) */;
both_r((int *)0,1) /*@ ghost ((int *)0,2) */;
+ /*@ ghost g_nothing(); */
+ /*@ ghost g_nothing_r(); */
+ /*@ ghost g_something_non_ghost((int *)0); */
+ /*@ ghost g_something_non_ghost_r((int *)0); */
+ /*@ ghost g_both((int *)0,1,(int *)0,2); */
+ /*@ ghost g_both_r((int *)0,1,(int *)0,2); */
return;
}
--
GitLab