Added a simple check for unused variables.

The check test whether the identifier is used at all in the
function and if not issue a warning. It is not tested whether the
usage is reachable at all, so

int i;
if (0)
  i;

would not generate a warning. This is the same as gcc/clang does.

The warning is disabled per default, but is active if -Wall is
given.

Bug 19872

5 files changed, 88 insertions, 2 deletions

diff --git a/cparser/Cerrors.ml b/cparser/Cerrors.ml
index dffd9c14..8b2a4cd5 100644
--- a/cparser/Cerrors.ml
+++ b/cparser/Cerrors.ml
@@ -88,6 +88,7 @@ type warning_type =
   | Unknown_pragmas
   | CompCert_conformance
   | Inline_asm_sdump
+  | Unused_variable
 
 (* List of active warnings *)
 let active_warnings: warning_type list ref = ref [
@@ -135,6 +136,7 @@ let string_of_warning = function
   | Unknown_pragmas -> "unknown-pragmas"
   | CompCert_conformance -> "compcert-conformance"
   | Inline_asm_sdump -> "inline-asm-sdump"
+  | Unused_variable -> "unused-variable"
 
 (* Activate the given warning *)
 let activate_warning w () =
@@ -179,6 +181,7 @@ let wall () =
     Unknown_pragmas;
     CompCert_conformance;
     Inline_asm_sdump;
+    Unused_variable
   ]
 
 let wnothing () =
@@ -207,6 +210,7 @@ let werror () =
     Unknown_pragmas;
     CompCert_conformance;
     Inline_asm_sdump;
+    Unused_variable;
   ]
 
 (* Generate the warning key for the message *)
@@ -368,6 +372,7 @@ let warning_options =
   error_option Unknown_pragmas @
   error_option CompCert_conformance @
   error_option Inline_asm_sdump @
+  error_option Unused_variable @
   [Exact ("-Wfatal-errors"), Set error_fatal;
    Exact ("-fdiagnostics-color"), Ignore; (* Either output supports it or no color *)
    Exact ("-fno-diagnostics-color"), Unset color_diagnostics;
diff --git a/cparser/Cerrors.mli b/cparser/Cerrors.mli
index 816b12b6..fb987bca 100644
--- a/cparser/Cerrors.mli
+++ b/cparser/Cerrors.mli
@@ -45,6 +45,7 @@ type warning_type =
   | Unknown_pragmas                (** unknown/unsupported pragma *)
   | CompCert_conformance           (** features that are not part of the CompCert C core language *)
   | Inline_asm_sdump               (** inline assembler used in combination of sdump *)
+  | Unused_variable                (** unused local variables *)
 
 val warning  : (string * int) -> warning_type -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a
 (** [warning (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as warining according to
diff --git a/cparser/Checks.ml b/cparser/Checks.ml
index 2e42cace..5ce51aba 100644
--- a/cparser/Checks.ml
+++ b/cparser/Checks.ml
@@ -14,6 +14,7 @@
 (* *********************************************************************)
 
 open C
+open Cerrors
 open Cutil
 
 let attribute_string = function
@@ -27,7 +28,7 @@ let unknown_attrs loc attrs =
   let unknown attr =
     let attr_class = class_of_attribute attr in
     if attr_class = Attr_unknown then
-      Cerrors.warning loc Cerrors.Unknown_attribute
+      warning loc Unknown_attribute
         "unknown attribute '%s' ignored" (attribute_string attr) in
   List.iter unknown attrs
 
@@ -93,3 +94,78 @@ let unknown_attrs_program p =
       in
         unknown_attrs_globdecls env' gl
   in unknown_attrs_globdecls (Builtins.environment()) p
+
+let rec vars_used_expr env e =
+  match e.edesc with
+  | EConst _
+  | ESizeof _
+  | EAlignof _ -> env
+  | EVar id -> IdentSet.add id env
+  | ECast (_,e)
+  | EUnop (_,e) -> vars_used_expr env e
+  | EBinop (_,e1,e2,_) ->
+    let env = vars_used_expr env e1 in
+    vars_used_expr env e2
+  | EConditional (e1,e2,e3) ->
+    let env = vars_used_expr env e1 in
+    let env = vars_used_expr env e2 in
+    vars_used_expr env e3
+  | ECompound (_,init) -> vars_used_init env init
+  | ECall (e,p) ->
+    let env = vars_used_expr env e in
+    List.fold_left vars_used_expr env p
+
+and vars_used_init env = function
+  | Init_single e -> vars_used_expr env e
+  | Init_array al -> List.fold_left vars_used_init env al
+  | Init_struct (_,sl) -> List.fold_left (fun env (_,i) -> vars_used_init env i) env sl
+  | Init_union (_,_,ui) -> vars_used_init env ui
+
+let rec vars_used_stmt ((dec_env,used_env) as acc) s =
+  match s.sdesc with
+  | Sbreak
+  | Scontinue
+  | Sgoto _
+  | Sreturn None
+  | Sskip -> acc
+  | Sreturn (Some e)
+  | Sdo e -> dec_env,(vars_used_expr used_env e)
+  | Sseq (s1,s2) ->
+    let acc = vars_used_stmt acc s1 in
+    vars_used_stmt acc s2
+  | Sif (e,s1,s2) ->
+    let used_env = vars_used_expr used_env e in
+    let acc = vars_used_stmt (dec_env,used_env) s1 in
+    vars_used_stmt acc s2
+  | Sfor (s1,e,s2,s3) ->
+    let used_env = vars_used_expr used_env e in
+    let acc = vars_used_stmt (dec_env,used_env) s1 in
+    let acc = vars_used_stmt acc s2 in
+    vars_used_stmt acc s3
+  | Sswitch (e,s)
+  | Swhile (e,s)
+  | Sdowhile (s,e) ->
+    let used_env = vars_used_expr used_env e in
+    vars_used_stmt (dec_env,used_env) s
+  | Sblock sl -> List.fold_left vars_used_stmt acc sl
+  | Sdecl (sto,id,ty,init) ->
+    let dec_env = IdentMap.add id s.sloc dec_env
+    and used_env = match init with
+      | Some init ->vars_used_init used_env init
+      | None -> used_env in
+    dec_env,used_env
+  | Slabeled (lbl,s) -> vars_used_stmt acc s
+  | Sasm (attr,str,op,op2,constr) ->
+    let vars_asm_op env (_,_,e) =
+      vars_used_expr env e in
+    let used_env = List.fold_left vars_asm_op used_env op in
+    let used_env = List.fold_left vars_asm_op used_env op2 in
+    dec_env,used_env
+
+let unused_variables p =
+  List.iter (fun g -> match g.gdesc with
+      | Gfundef fd ->
+        let dec_env,used_env = vars_used_stmt (IdentMap.empty,IdentSet.empty) fd.fd_body in
+        IdentMap.iter (fun id loc -> if not (IdentSet.mem id used_env) then
+                          warning loc Unused_variable "unused variable '%s'" id.name) dec_env
+      | _ -> ()) p
diff --git a/cparser/Checks.mli b/cparser/Checks.mli
index 1566d6e4..4d61a5b8 100644
--- a/cparser/Checks.mli
+++ b/cparser/Checks.mli
@@ -14,3 +14,5 @@
 (* *********************************************************************)
 
 val unknown_attrs_program: C.program -> unit
+
+val unused_variables: C.program -> unit
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 02980529..d75e2410 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -2673,4 +2673,6 @@ let _ = elab_funbody_f := elab_funbody
 let elab_file prog =
   reset();
   ignore (elab_definitions false (Builtins.environment()) prog);
-  elaborated_program()
+  let p = elaborated_program () in
+  Checks.unused_variables p;
+  p