## 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 (that disappears after manually removing \ghost attribute). [f_cut.c](/uploads/90f52009ec5f1412c371349b3fca3659/f_cut.c) Here is the example ``` // Run frama-c on this file and pretty-print it: // frama-c f_cut.c -print -no-unicode -ocode f_cut_printed.c // Run on the resulting pretty-printed file: // frama-c f_cut_printed.c typedef unsigned char uint8; typedef unsigned short uint16; typedef unsigned long uint32; uint8 Array[10]; /*@ ghost uint32 FCG_Number; */ /*@ ghost uint32 FCG_Var1[1000]; */ /*@ ghost uint32 FCG_Var2[1000]; */ /*@ predicate mypredl{L}= (\forall integer MyNum; 0 <= MyNum < FCG_Number ==> FCG_Var2[MyNum] == ((uint16)(*((uint8 *)(&Array[FCG_Var1[MyNum]] + (1))) * 256 + *((uint8 *)((&Array[FCG_Var1[MyNum]] + (1 + 2)) + 1)))) ) ; */ ``` Here is the error message: ``` [kernel] Parsing f_cut_printed.c (with preprocessing) [kernel:annot-error] f_cut_printed.c:14: Warning: unexpected token '\ghost' [kernel] User Error: warning annot-error treated as fatal error. [kernel] User Error: stopping on file "f_cut_printed.c" that has errors. Add '-kernel-msg-key pp' for preprocessing command. [kernel] Frama-C aborted: invalid user input. ```