diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 7f5b53a7cd886e40910c5a6f71ce238aa23bd5d7..a1b92d74b0f47a9960b240d112be21f26fd1b6ab 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -4993,11 +4993,20 @@ and doType (ghost:bool) isFuncArg
           (args', !newisva)
         end else (args, isva)
       in
+      let argl_length = List.length args' in
       (* Make the argument as for a formal *)
       let doOneArg (s, (n, ndt, a, cloc)) : varinfo =
         let s' = doSpecList ghost n s in
         let vi = makeVarInfoCabs ~ghost ~isformal:true ~isglobal:false
             (convLoc cloc) s' (n,ndt,a) in
+        if isVoidType vi.vtype then begin
+          if argl_length > 1 then
+            Kernel.error ~once:true ~current:true
+              "'void' must be the only parameter if specified";
+          if vi.vname <> "" then
+            Kernel.error ~once:true ~current:true
+              "named parameter '%s' has void type" vi.vname
+        end;
         (* Add the formal to the environment, so it can be referenced by
            other formals  (e.g. in an array type, although that will be
            changed to a pointer later, or though typeof).  *)
diff --git a/tests/syntax/oracle/void_parameter.res.oracle b/tests/syntax/oracle/void_parameter.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..651f5588fe9f3411eff4dafddd92595c57b2a204
--- /dev/null
+++ b/tests/syntax/oracle/void_parameter.res.oracle
@@ -0,0 +1,19 @@
+[kernel] Parsing tests/syntax/void_parameter.i (no preprocessing)
+[kernel] tests/syntax/void_parameter.i:7: User Error: 
+  named parameter 'parameter' has void type
+[kernel] tests/syntax/void_parameter.i:8: User Error: 
+  'void' must be the only parameter if specified
+[kernel] tests/syntax/void_parameter.i:9: User Error: 
+  'void' must be the only parameter if specified
+[kernel] tests/syntax/void_parameter.i:9: User Error: 
+  named parameter 'parameter' has void type
+[kernel] tests/syntax/void_parameter.i:13: User Error: 
+  named parameter 'parameter' has void type
+[kernel] tests/syntax/void_parameter.i:14: User Error: 
+  'void' must be the only parameter if specified
+[kernel] tests/syntax/void_parameter.i:15: User Error: 
+  'void' must be the only parameter if specified
+[kernel] tests/syntax/void_parameter.i:15: User Error: 
+  named parameter 'parameter' has void type
+[kernel] User Error: stopping on file "tests/syntax/void_parameter.i" that has errors.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/void_parameter.i b/tests/syntax/void_parameter.i
new file mode 100644
index 0000000000000000000000000000000000000000..f4a14535232ca14a6f0ea5fb00d4009aa6d75018
--- /dev/null
+++ b/tests/syntax/void_parameter.i
@@ -0,0 +1,16 @@
+/* run.config
+
+*/
+
+// GCC warning, Clang/CompCert error
+void f1(void);
+void f2(void parameter);
+void f3(void, int x);
+void f4(void parameter, int x);
+
+// GCC/Clang/CompCert error
+void f1(void){}
+void f2(void parameter){}
+void f3(void, int x){}
+void f4(void parameter, int x){}
+