From 92480bd598f863d9e960f04fa4a45940522a52d2 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 22 Jan 2021 09:55:36 +0100
Subject: [PATCH] [aorai] fixes assigns in test serial.c
---
src/plugins/aorai/tests/ya/serial.c | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/plugins/aorai/tests/ya/serial.c b/src/plugins/aorai/tests/ya/serial.c
index 3bf7ab6cfac..98795b7b3d5 100644
--- a/src/plugins/aorai/tests/ya/serial.c
+++ b/src/plugins/aorai/tests/ya/serial.c
@@ -17,13 +17,13 @@ OPT: -cpp-extra-args="-DFOR_WP" -aorai-automata @PTEST_DIR@/@PTEST_NAME@_wp.ya -
#define BW_AND3 <=
#endif
-/*@ assigns \result \from \nothing;
+/*@ assigns \result,Frama_C_entropy_source \from Frama_C_entropy_source;
ensures 0 <= \result < 0x100; */
int input_status(void) {
return Frama_C_interval(0x00, 0xff);
}
-/*@ assigns \result \from \nothing;
+/*@ assigns \result,Frama_C_entropy_source \from Frama_C_entropy_source;
ensures 0 <= \result < 0x100; */
int input_data(void) {
return Frama_C_interval(0x00, 0xff);
--
GitLab