Fix merging and renaming of inlines

README.md

@@ -52,6 +52,10 @@ commands to build and test `goblint-cil`:
     dune build
     dune runtest    # runs the regression test suite
 
+To run a single test go to the build directory (e.g. `_build/default/test`) and run e.g.:
+
+    dune exec -- make test/array1
+
 You can also install `goblint-cil` into the opam switch:
 
     dune build @install

doc/cil.tex

@@ -2106,6 +2106,10 @@ \subsection{Code that CIL won't compile}
 \subsection{Code that behaves differently under CIL}
 
 \begin{itemize}
+\item Without optimizations GCC generally does not use ``inline'' functions.
+With optimizations they might be inlined. CIL assumes optimization, and also
+assumes that ``inline'' functions are always inlined.
+
 \item GCC has a strange feature called ``extern inline''. Such a function can
 be defined twice: first with the ``extern inline'' specifier and the second
 time without it. If optimizations are turned off then the ``extern inline''
@@ -2357,7 +2361,11 @@ \subsection{Effects of the CIL translation}
   --mode=xxx   What tool to emulate:
                 GNUCC     - GNU CC
                 MSVC      - MS VC cl compiler
-
+  --cstd=xxx   What C standard / GNU dialect to emulate:
+                c90 (also used for c89, iso9899:1990, iso9899:199409, gnu90, gnu89)
+                c99 (also used for c9x, iso9899:1999, iso9899:199x, gnu99, gnu9x)
+                c11 (c1x, iso9899:2011, c17, c18, iso9899:2017, iso9899:2018, c2x, gnu11, gnu1x, gnu17, gnu18, gnu2x)
+  --gnu89inline gnu89 semantic for inline functions
   --dest=xxx   The destination directory. Will make one if it does not exist
   --patch=xxx  Patch file (can be specified multiple times)
   --ppargs=xxx An argument to be passed to the preprocessor (can be specified

lib/perl5/App/Cilly.pm.in

@@ -361,6 +361,11 @@ Options:
                 AR      - GNU ar
                This option must be the first one! If it is not found there
                then GNUCC mode is assumed.
+  --cstd=xxx   What C standard / GNU dialect to emulate:
+                c90 (also used for c89, iso9899:1990, iso9899:199409, gnu90, gnu89)
+                c99 (also used for c9x, iso9899:1999, iso9899:199x, gnu99, gnu9x)
+                c11 (c1x, iso9899:2011, c17, c18, iso9899:2017, iso9899:2018, c2x, gnu11, gnu1x, gnu17, gnu18, gnu2x)
+  --gnu89inline gnu89 semantic for inline functions
   --help (or -help) Prints this help message.
   --verbose    Prints a lot of information about what is being done.
   --save-temps Keep temporary files in the current directory.
@@ -1517,12 +1522,34 @@ sub new {
 	    # skipping -###, --help, --target-help, --version
 
 	    # C Language Options
-            "-ansi" => { TYPE => 'ALLARGS' },
-            '-std=' => { TYPE => 'ALLARGS' },
+      "-ansi" => {
+            TYPE => 'ALLARGS',
+            RUN => sub {
+                push @{$stub->{CILARGS}}, "--cstd", "c90";
+            }},
+      "-std=(c90|c89|iso9899:1990|iso9899:199409|gnu90|gnu89)" => {
+            TYPE => 'ALLARGS',
+            RUN => sub {
+                push @{$stub->{CILARGS}}, "--cstd", "c90";
+            }},
+      "-std=(c99|c9x|iso9899:1999|iso9899:199x|gnu99|gnu9x)" => {
+            TYPE => 'ALLARGS',
+            RUN => sub {
+                push @{$stub->{CILARGS}}, "--cstd", "c99";
+            }},
+      "-std=(c1x|iso9899:2011|c17|c18|iso9899:2017|iso9899:2018|c2x|gnu11|gnu1x|gnu17|gnu18|gnu2x)" => {
+            TYPE => 'ALLARGS',
+            RUN => sub {
+                push @{$stub->{CILARGS}}, "--cstd", "c11";
+            }},
+      "-fgnu89-inline" => {
+            RUN => sub {
+                push @{$stub->{CILARGS}}, "--gnu89inline";
+            }},
 	    "-aux-info\$" => { TYPE => 'CC', ONEMORE => 1 },
-             # GCC might define some more macros, eg. for -fPIC, so pass
-             # the -f to the preprocessor and the compiler
-            "-f" => { TYPE => 'ALLARGS' },
+            # GCC might define some more macros, eg. for -fPIC, so pass
+            # the -f to the preprocessor and the compiler
+      "-f" => { TYPE => 'ALLARGS' },
 
 	    # -Wx,blah options (placed before general -W warning options)
             #matth: the handling of -Wp may be wrong.  We may need to

lib/perl5/patcher

@@ -66,7 +66,6 @@ options:
   --verbose    Prints a lot of information about what is being done
   --mode=xxx   What tool to emulate:
                 GNUCC   - GNU CC
-
   --dest=xxx   The destination directory. Will make one if it does not exist
   --patch=xxx  Patch file (can be specified multiple times)
 
@@ -94,9 +93,9 @@ my %option;
      "--verbose|v",       # Display information about programs invoked
      "--mode=s",          # The mode (GNUCC)
      "--dest=s",          # The destination directory
-     "--patch=s@",         # Patch files
-     "--ufile=s@",         # User include files
-     "--sfile=s@",         # System include files
+     "--patch=s@",        # Patch files
+     "--ufile=s@",        # User include files
+     "--sfile=s@",        # System include files
      "--stdoutpp",        # pp to stdout
      "--skipmissing",
      "--dumpversion",

src/cil.ml

@@ -55,11 +55,15 @@ module IH = Inthash
    information in configure.in *)
 let cilVersion         = Cilversion.cilVersion
 
-(* A few globals that control the interpretation of C source *)
-let msvcMode = ref false              (* Whether the pretty printer should
-                                         print output for the MS VC
-                                         compiler. Default is GCC *)
-let c99Mode = ref true (* True to handle ISO C 99 vs 90 changes.
+type cstd = C90 | C99 | C11
+let cstd_of_string = function
+| "c90" -> C90
+| "c99" -> C99
+| "c11" -> C11
+| _ -> failwith "Not a valid c standard argument."
+let cstd = ref C99
+let gnu89inline = ref false
+let c99Mode () = !cstd <> C90 (* True to handle ISO C 99 vs 90 changes.
       c99mode only affects parsing of decimal integer constants without suffix
           a) on machines where long and long long do not have the same size
              (e.g. 32 Bit machines, 64 Bit Windows, not 64 Bit MacOS or (most? all?) 64 Bit Linux):
@@ -2775,7 +2779,7 @@ let parseInt (str: string) : exp =
       1, [IUInt; IULong; IULongLong]
     else
       0, if octalhex then [IInt; IUInt; ILong; IULong; ILongLong; IULongLong]
-      else if not !c99Mode then [ IInt; ILong; IULong; ILongLong; IULongLong]
+      else if not (c99Mode ()) then [ IInt; ILong; IULong; ILongLong; IULongLong]
       else [IInt; ILong; ILongLong]
       (* c99mode only affects parsing of decimal integer constants without suffix
           a) on machines where long and long long do not have the same size
@@ -4298,13 +4302,10 @@ class defaultCilPrinterClass : cilPrinter = object (self)
     | "const", [] -> nil, false (* don't print const directly, because of split local declarations *)
     | "pconst", [] -> text "const", false (* pconst means print const *)
           (* Put the aconst inside the attribute list *)
-    | "complex", [] when !c99Mode -> text "_Complex", false
+    | "complex", [] when (c99Mode ()) -> text "_Complex", false
     | "complex", [] -> text "__complex__", false
     | "aconst", [] -> text "__const__", true
     | "thread", [] -> text "__thread", false
-(*
-    | "used", [] when not !msvcMode -> text "__attribute_used__", false
-*)
     | "volatile", [] -> text "volatile", false
     | "restrict", [] -> text "__restrict", false
     | "missingproto", [] -> text "/* missing proto */", false

src/cil.mli

@@ -53,6 +53,11 @@ val initCIL: unit -> unit
    M.m.r (major, minor and release) *)
 val cilVersion: string
 
+type cstd = C90 | C99 | C11
+val cstd_of_string: string -> cstd
+val cstd: cstd ref
+val gnu89inline: bool ref
+
 (** This module defines the abstract syntax of CIL. It also provides utility
    functions for traversing the CIL data structures, and pretty-printing
    them. The parser can be invoked as
@@ -2021,10 +2026,6 @@ val visitCilAttributes: cilVisitor -> attribute list -> attribute list
 
 (** {b Utility functions} *)
 
-(** Whether the pretty printer should print output for the MS VC compiler.
-   Default is GCC. After you set this function you should call {!initCIL}. *)
-val msvcMode: bool ref
-
 (** Whether to convert local static variables into global static variables *)
 val makeStaticGlobal: bool ref
 

src/ciloptions.ml

@@ -6,7 +6,7 @@
     Wes Weimer          <[email protected]>
     Ben Liblit          <[email protected]>
    All rights reserved.
-   
+
    Redistribution and use in source and binary forms, with or without
    modification, are permitted provided that the following conditions are
    met:
@@ -39,16 +39,16 @@
 open GoblintCil
 module E = Errormsg
 
-let setDebugFlag v name = 
+let setDebugFlag v name =
   E.debugFlag := v;
   if v then Pretty.flushOften := true
 
-type outfile = 
+type outfile =
     { fname: string;
-      fchan: out_channel } 
+      fchan: out_channel }
 
       (* Processign of output file arguments *)
-let openFile (what: string) (takeit: outfile -> unit) (fl: string) = 
+let openFile (what: string) (takeit: outfile -> unit) (fl: string) =
   if !E.verboseFlag then
     ignore (Printf.printf "Setting %s to %s\n" what fl);
   (try takeit { fname = fl;
@@ -58,44 +58,44 @@ let openFile (what: string) (takeit: outfile -> unit) (fl: string) =
 
 
 let fileNames : string list ref = ref []
-let recordFile fname = 
-  fileNames := fname :: (!fileNames) 
+let recordFile fname =
+  fileNames := fname :: (!fileNames)
 
                          (* Parsing of files with additional names *)
-let parseExtraFile (s: string) = 
+let parseExtraFile (s: string) =
   try
     let sfile = open_in s in
     while true do
       let line = try input_line sfile with e -> (close_in sfile; raise e) in
       let linelen = String.length line in
       let rec scan (pos: int) (* next char to look at *)
-          (start: int) : unit (* start of the word, 
+          (start: int) : unit (* start of the word,
                                  or -1 if none *) =
-        if pos >= linelen then 
-          if start >= 0 then 
+        if pos >= linelen then
+          if start >= 0 then
             recordFile (String.sub line start (pos - start))
-          else 
+          else
             () (* Just move on to the next line *)
         else
           let c = String.get line pos in
-          match c with 
-            ' ' | '\n' | '\r' | '\t' -> 
+          match c with
+            ' ' | '\n' | '\r' | '\t' ->
               (* whitespace *)
               if start >= 0 then begin
                 recordFile (String.sub line start (pos - start));
               end;
               scan (pos + 1) (-1)
-                
+
           | _ -> (* non-whitespace *)
-              if start >= 0 then 
-                scan (pos + 1) start 
+              if start >= 0 then
+                scan (pos + 1) start
               else
                 scan (pos + 1) pos
       in
         scan 0 (-1)
     done
   with Sys_error _ -> E.s (E.error "Cannot find extra file: %s" s)
-  |  End_of_file -> () 
+  |  End_of_file -> ()
 
 
 let options : (string * Arg.spec * string) list =
@@ -130,7 +130,7 @@ let options : (string * Arg.spec * string) list =
     Arg.Clear E.warnFlag,
     (" Disable optional warnings" ^ is_default (not !E.warnFlag));
 
-    "--noTruncateWarning", 
+    "--noTruncateWarning",
     Arg.Clear Cil.warnTruncate,
     " Suppress warning about truncating integer constants";
 
@@ -165,7 +165,15 @@ let options : (string * Arg.spec * string) list =
     "--strictcheck", Arg.Unit (fun _ -> Cilutil.doCheck := true;
                                         Cilutil.strictChecking := true),
                      " Same as --check, but treats problems as errors not warnings.";
-    "", Arg.Unit (fun _ -> ()), "";
+
+    "--cstd", Arg.String (fun s -> Cil.cstd := Cil.cstd_of_string s),
+                      " Specify the c language standard. Choose between c90, c99, c11";
+
+    "--gnu89inline", Arg.Set Cil.gnu89inline,
+                      " Use gnu89 semantic for inlining";
+
+    "--mergeinlines", Arg.Unit (fun _ -> Mergecil.merge_inlines := true),
+                      " Try to merge definitions of inline functions.";
 
     "--noPrintLn",
     Arg.Unit (fun _ ->
@@ -179,11 +187,11 @@ let options : (string * Arg.spec * string) list =
                 Cprint.printLnComment := true),
     " Print #line directives in the output, but put them in comments";
 
-    "--commPrintLnSparse", 
+    "--commPrintLnSparse",
     Arg.Unit (fun _ ->
                 Cil.lineDirectiveStyle := Some Cil.LineCommentSparse;
                 Cprint.printLnComment := true),
-    " Print commented #line directives in the output only when\n\t\t\t\tthe line number changes.";
+    " Print commented #line directives in the output only when the line number changes.";
 
     "--stats",
     Arg.Set Cilutil.printStats,
@@ -204,7 +212,7 @@ let options : (string * Arg.spec * string) list =
      try
        let machineModel = Sys.getenv "CIL_MACHINE" in
        Cil.envMachine := Some (Machdepenv.modelParse machineModel);
-     with 
+     with
        Not_found ->
 	 ignore (E.error "CIL_MACHINE environment variable is not set")
      | Failure msg ->
@@ -233,7 +241,7 @@ let options : (string * Arg.spec * string) list =
 
     "--extrafiles",
     Arg.String parseExtraFile,
-    "<filename> File that contains a list of additional files to process,\n\t\t\t\tseparated by newlines";
+    "<filename> File that contains a list of additional files to process, separated by newlines";
 
     (* Lowering Options *)
     "", Arg.Unit (fun () -> ()), " \n\t\tLowering Options\n";
@@ -292,13 +300,13 @@ let options : (string * Arg.spec * string) list =
 
     "--useLogicalOperators",
     Arg.Set Cil.useLogicalOperators,
-    (" Where possible (that is, if there are no side-effects),\n\t\t\t\t" ^
+    (" Where possible (that is, if there are no side-effects)," ^
        "retain &&, || and ?: (instead of transforming them to If statements)" ^
        is_default !Cil.useLogicalOperators);
 
     "--noUseLogicalOperators",
     Arg.Clear Cil.useLogicalOperators,
-     ("Transform &&, || and ?: to If statements" ^
+     (" Transform &&, || and ?: to If statements" ^
        is_default (not !Cil.useLogicalOperators));
 
     "--useComputedGoto",
@@ -351,7 +359,7 @@ let options : (string * Arg.spec * string) list =
 
     "--noPrintCilAsIs",
     Arg.Clear Cil.printCilAsIs,
-    (" Simplify the CIL when printing.  This produces prettier output\n\t\t\t\tby e.g. changing while(1) into more meaningful loops  " ^ is_default (not !Cil.printCilAsIs));
+    (" Simplify the CIL when printing. This produces prettier output by e.g. changing while(1) into more meaningful loops" ^ is_default (not !Cil.printCilAsIs));
 
     "--noWrap",
     Arg.Unit (fun _ -> Cil.lineLength := 100_000),

src/cilutil.ml

@@ -1,11 +1,11 @@
 (*
 
-   Copyright (c) 2001-2002, 
+   Copyright (c) 2001-2002,
     George C. Necula    <[email protected]>
     Scott McPeak        <[email protected]>
     Wes Weimer          <[email protected]>
    All rights reserved.
-   
+
    Redistribution and use in source and binary forms, with or without
    modification, are permitted provided that the following conditions are
    met:

src/main.ml

@@ -169,10 +169,10 @@ let theMain () =
         [
           "--out", Arg.String (openFile "output"
                                  (fun oc -> outChannel := Some oc)),
-              " the name of the output CIL file.\n\t\t\t\tThe cilly script sets this for you.";
+              " The name of the output CIL file. The cilly script sets this for you.";
           "--mergedout", Arg.String (openFile "merged output"
                                        (fun oc -> mergedChannel := Some oc)),
-              " specify the name of the merged file";
+              " Specify the name of the merged file";
           "--load", Arg.String ignore, "" (* ignore --load because they have been processed above already *)
         ]
         @ F.args @ featureArgs in