diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml
index a596fa02ee7f098980ea4cab714e14b823a564d0..a2cdec06341601b2e2f0602b099678f4e06a3532 100644
--- a/src/kernel_services/ast_queries/cil_builtins.ml
+++ b/src/kernel_services/ast_queries/cil_builtins.ml
@@ -77,7 +77,7 @@ let () = add_special_builtin_family
     (fun s -> Datatype.String.Set.mem s !special_builtins_table)
 
 let () = List.iter add_special_builtin
-    [ "__builtin_stdarg_start"; "__builtin_va_arg";
+    [ "__builtin_stdarg_start"; "__builtin_va_arg"; "__builtin_va_end";
       "__builtin_va_start"; "__builtin_expect"; "__builtin_next_arg"; ]
 
 module Builtin_functions =