## Contextual information: currently used versions - Frama-C installation mode: *Opam* - Frama-C version 26.0beta - MetAcsl 0.4beta - Alt-Ergo 2.3.2 - OS name: *Ubuntu* - OS version: *20.04* ## The issue On the attached file, after parsing and printing the code, running frama-c again to parse the code produces an error (due to missing parentheses in ranges). [f.c](/uploads/dac68b95adf9d3c2c83b7b3ec9ce5898/f.c) Here is the example ``` // Run frama-c on this file and pretty-print it: // frama-c f.c -print -no-unicode -ocode f_printed.c // Run on the resulting pretty-printed file: // frama-c f_printed.c typedef unsigned char uchar; typedef unsigned long ulong; typedef unsigned char *pchar; uchar *Ref; uchar Array[100]; /*@ ghost ulong FCG_Var1[1000]; */ /*@ ensures sep1: \let Ref_range = Ref + (0 .. (1 << (size)) - 1); \let PROP = \forall integer MyNum; \let myrange = (0 .. (6 - 1)); \let Var2 = &Array[FCG_Var1[MyNum]]; \let CASE_i = 0 <= MyNum < 10; \let PROP_i = \separated(Ref_range, Var2 + myrange); CASE_i ==> PROP_i; PROP; */ static uchar myfun(pchar p_array, short index, uchar size) { uchar __retres; return __retres; } ``` Here is the error message: ``` [kernel] Parsing f_printed.c (with preprocessing) [kernel:annot-error] f_printed.c:11: Warning: unexpected token '..' [kernel] User Error: warning annot-error treated as fatal error. [kernel] User Error: stopping on file "f_printed.c" that has errors. Add '-kernel-msg-key pp' for preprocessing command. [kernel] Frama-C aborted: invalid user input. ```