### Steps to reproduce the issue 1. Instrument and compile the input file at_label_Init.c using the command: e-acsl-gcc.sh -c at_label_Init.c 2. Execute the generated file: ./a.out.e-acsl The content of at_label_Init.c is as follows: ```C int global_var = 0; /*@ ensures \result == \at(global_var, Init); */ // Test 3: Should pass int get_init_state() { return 0; } /*@ ensures \at(global_var, Init) == 0; // Test 1: Should pass ensures global_var == 10; */ void test_init_label() { global_var = 10; } int main() { /*@ assert \at(global_var, Init) == 0; */ test_init_label(); /*@ assert \at(global_var, Init) == 0; */ // Test 2: Should pass int init_val = get_init_state(); /*@ assert init_val == 0; */ return 0; } ``` ### Expected behaviour The execution of ./a.out.e-acsl should terminate normally without any output. All ACSL annotations should be satisfied, as the Init label is permitted in all annotations and, according to the manual frama-c-acsl-implementation.pdf, refers to the program state before the call to main. ### Actual behaviour When individually testing all three annotations marked with Test X (where X = 1, 2, 3), the execution of ./a.out.e-acsl reports errors and terminates with "Aborted (core dumped)": - For Test 1 and 3: Error: Postcondition failed - For Test 2: Error: Assertion failed. The E-ACSL plugin incorrectly evaluates all three annotations as unsatisfied. ### Contextual information - Frama-C installation mode: Opam - Frama-C version: 31.0 (Gallium) - Plug-in used: E-ACSL - OS name: WSL 2 - OS version: Windows 11, Ubuntu 24.04 Reported on behalf of Wenjian Chai (chaiwj@ios.ac.cn)