diff --git a/goblint.opam b/goblint.opam index 8c369b5381..7027f58b66 100644 --- a/goblint.opam +++ b/goblint.opam @@ -74,7 +74,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git" # also remember to generate/adjust goblint.opam.locked! available: os-distribution != "alpine" & arch != "arm64" pin-depends: [ - [ "goblint-cil.2.0.0" "git+https://github.com/goblint/cil.git#3d079de2568eba596e821f8efb1db292bbfe104c" ] + [ "goblint-cil.2.0.0" "git+https://github.com/goblint/cil.git#56a58af3aa160ae64759fa1c893b08a4148eeb9c" ] # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252) [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ] # TODO: add back after release, only pinned for CI stability diff --git a/goblint.opam.locked b/goblint.opam.locked index b288ea1b69..08ca53ae98 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -124,7 +124,7 @@ available: os-distribution != "alpine" & arch != "arm64" pin-depends: [ [ "goblint-cil.2.0.0" - "git+https://github.com/goblint/cil.git#3d079de2568eba596e821f8efb1db292bbfe104c" + "git+https://github.com/goblint/cil.git#56a58af3aa160ae64759fa1c893b08a4148eeb9c" ] [ "apron.v0.9.13" diff --git a/goblint.opam.template b/goblint.opam.template index 9e0286b21e..95157ecfbe 100644 --- a/goblint.opam.template +++ b/goblint.opam.template @@ -2,7 +2,7 @@ # also remember to generate/adjust goblint.opam.locked! available: os-distribution != "alpine" & arch != "arm64" pin-depends: [ - [ "goblint-cil.2.0.0" "git+https://github.com/goblint/cil.git#3d079de2568eba596e821f8efb1db292bbfe104c" ] + [ "goblint-cil.2.0.0" "git+https://github.com/goblint/cil.git#56a58af3aa160ae64759fa1c893b08a4148eeb9c" ] # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252) [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ] # TODO: add back after release, only pinned for CI stability diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml index 9f2a54ab03..576bcd5ee7 100644 --- a/src/util/cilfacade.ml +++ b/src/util/cilfacade.ml @@ -19,7 +19,9 @@ let isFloatType t = | _ -> false let init_options () = - Mergecil.merge_inlines := get_bool "cil.merge.inlines" + Mergecil.merge_inlines := get_bool "cil.merge.inlines"; + Cil.cstd := Cil.cstd_of_string (get_string "cil.cstd"); + Cil.gnu89inline := get_bool "cil.gnu89inline" let init () = initCIL (); diff --git a/src/util/options.schema.json b/src/util/options.schema.json index 00f68fb619..4f654bd0a5 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -263,6 +263,19 @@ } }, "additionalProperties": false + }, + "cstd": { + "title": "cil.cstd", + "type": "string", + "description": "Specify the c standard used for parsing.", + "default": "c99", + "enum": ["c90", "c99", "c11"] + }, + "gnu89inline": { + "title": "cil.gnu89inline", + "type": "boolean", + "description": "Indicates whether gnu89 semantic should be used for inline functions.", + "default": false } }, "additionalProperties": false