Skip to content
Snippets Groups Projects
Commit 92480bd5 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[aorai] fixes assigns in test serial.c

parent 8e67886e
No related branches found
No related tags found
No related merge requests found
...@@ -17,13 +17,13 @@ OPT: -cpp-extra-args="-DFOR_WP" -aorai-automata @PTEST_DIR@/@PTEST_NAME@_wp.ya - ...@@ -17,13 +17,13 @@ OPT: -cpp-extra-args="-DFOR_WP" -aorai-automata @PTEST_DIR@/@PTEST_NAME@_wp.ya -
#define BW_AND3 <= #define BW_AND3 <=
#endif #endif
/*@ assigns \result \from \nothing; /*@ assigns \result,Frama_C_entropy_source \from Frama_C_entropy_source;
ensures 0 <= \result < 0x100; */ ensures 0 <= \result < 0x100; */
int input_status(void) { int input_status(void) {
return Frama_C_interval(0x00, 0xff); 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; */ ensures 0 <= \result < 0x100; */
int input_data(void) { int input_data(void) {
return Frama_C_interval(0x00, 0xff); return Frama_C_interval(0x00, 0xff);
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment