Merge pull request #129 from just-max/add-return-on-noreturn-fallthrough

Add `return` statements in `noreturn` functions

Author: michael-schwarz

src/cil.ml

@@ -88,6 +88,8 @@ let useComputedGoto = ref false
 
 let useCaseRange = ref false
 
+let addReturnOnNoreturnFallthrough = ref false
+
 module M = Machdep
 (* Cil.initCil will set this to the current machine description.
    Makefile.cil generates the file src/machdep.ml,

src/cil.mli

@@ -57,6 +57,7 @@ type cstd = C90 | C99 | C11
 val cstd_of_string: string -> cstd
 val cstd: cstd ref
 val gnu89inline: bool ref
+val addReturnOnNoreturnFallthrough: bool ref
 
 (** This module defines the abstract syntax of CIL. It also provides utility
    functions for traversing the CIL data structures, and pretty-printing

src/frontc/cabs2cil.ml

@@ -6437,8 +6437,14 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function
                     ignore (warn "Body of function %s falls-through and cannot find an appropriate return value" !currentFunctionFDEC.svar.vname);
                     None
               in
-              if not (hasAttribute "noreturn"
-                        !currentFunctionFDEC.svar.vattr) then
+              if
+                (* By default, (addReturnOnNoreturnFallthrough = false), CIL does not add a return statement
+                  in functions marked noreturn. However, unlike functions that are detected to never fall through,
+                  the end of these functions can possibly be reached (perhaps in buggy program code), so with
+                  the option set to true, always add the return statement. *)
+                !addReturnOnNoreturnFallthrough
+                || not (hasAttribute "noreturn" !currentFunctionFDEC.svar.vattr)
+              then
                 !currentFunctionFDEC.sbody.bstmts <-
                   !currentFunctionFDEC.sbody.bstmts
                   @ [mkStmt (Return(retval, endloc))]