E-ACSL : non-existent assigns clause in behavior
Steps to reproduce the issue
Run the following code with E-ACSL using e-acsl-gcc.sh -c -O assigns_test.out assigns_test.c
:
/* assigns_test.c */
#include <limits.h>
int global_int;
/*@
requires INT_MIN < global_int < INT_MAX;
assigns global_int;
*/
int abs_global(){
if(global_int < 0) {return -global_int;}
return global_int;
}
int main(){
global_int = 0;
int local_int = abs_global();
return local_int;
}
Expected behaviour
Instrumentation happens without warning.
Actual behaviour
The following warning [e-acsl] assigns_test.c:9: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
is reported, despite the function contract of abs_global
not featuring any behavior.
Contextual information
- Frama-C installation mode: Opam
- Frama-C version: at least from 26, still there in 28~beta
- Plug-in used: E-ACSL
- OS name: Ubuntu (via WSL)
- OS version: 22.04.2 LTS
FYI @nkosmatov