Skip to content

Use C standard option also for preprocessing #1807

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
sim642 merged 4 commits into from
Sep 5, 2025
Merged

Use C standard option also for preprocessing #1807

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
7595e10
Add more values to cil.cstd
sim642 Aug 14, 2025
42bddbd
Use cil.cstd option for preprocessing as well
sim642 Aug 14, 2025
c4e4a32
Make gnu11 default cil.cstd
sim642 Aug 14, 2025
8b39137
Rename cil.cstd option to std
sim642 Aug 14, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 10 additions & 1 deletion src/common/util/cilfacade.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,16 @@ let is_first_field x = match x.fcomp.cfields with

let init_options () =
Mergecil.merge_inlines := get_bool "cil.merge.inlines";
Cil.cstd := Cil.cstd_of_string (get_string "cil.cstd");
Cil.cstd := (
match get_string "std" with
| "c89" | "c90"
| "gnu89" | "gnu90" -> C90
| "c99" | "c9x"
| "gnu99" | "gnu9x" -> C99
| "c11" | "c1x"
| "gnu11" | "gnu1x" -> C11
| _ -> assert false
);
Cil.gnu89inline := get_bool "cil.gnu89inline";
Cabs2cil.addNestedScopeAttr := get_bool "cil.addNestedScopeAttr";

Expand Down
21 changes: 14 additions & 7 deletions src/config/options.schema.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -171,6 +171,20 @@
"type": "string",
"default": ".goblint"
},
"std": {
"title": "std",
"type": "string",
"description": "Specify the c standard used for preprocessing and parsing.",
"default": "gnu11",
"enum": [
"c89", "c90",
"gnu89", "gnu90",
"c99", "c9x",
"gnu99", "gnu9x",
"c11", "c1x",
"gnu11", "gnu1x"
]
},
"pre": {
"title": "Preprocessing",
"description": "Preprocessing options",
Expand Down Expand Up @@ -276,13 +290,6 @@
},
"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",
Expand Down
2 changes: 2 additions & 0 deletions src/maingoblint.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -267,6 +267,8 @@ let preprocess_files () =
(* Preprocessor flags *)
let cppflags = ref (get_string_list "pre.cppflags") in

cppflags := ("--std=" ^ get_string "std") :: !cppflags;

if get_bool "ana.sv-comp.enabled" then (
let architecture_flag = match get_string "exp.architecture" with
| "32bit" -> "-m32"
Expand Down
Loading