{
  "$schema": "http://json-schema.org/draft-04/schema#",
  "type": "object",
  "properties": {
    "files": {
      "title": "files",
      "description": "Files to analyze.",
      "type": "array",
      "items": {
        "type": "string"
      },
      "default": []
    },
    "outfile": {
      "title": "outfile",
      "description": "File to print output to.",
      "type": "string",
      "default": ""
    },
    "justcil": {
      "title": "justcil",
      "description": "Just parse and output the CIL.",
      "type": "boolean",
      "default": false
    },
    "justcfg": {
      "title": "justcfg",
      "description": "Only output the CFG in cfg.dot .",
      "type": "boolean",
      "default": false
    },
    "verify": {
      "title": "verify",
      "description":
        "Verify that the solver reached a post-fixpoint. Beware that disabling this also disables output of warnings since post-processing of the results is done in the verification phase!",
      "type": "boolean",
      "default": true
    },
    "mainfun": {
      "title": "mainfun",
      "description": "Sets the name of the main functions.",
      "type": "array",
      "items": { "type": "string" },
      "default": [ "main" ]
    },
    "exitfun": {
      "title": "exitfun",
      "description": "Sets the name of the cleanup functions.",
      "type": "array",
      "items": { "type": "string" },
      "default": []
    },
    "otherfun": {
      "title": "otherfun",
      "description": "Sets the name of other functions.",
      "type": "array",
      "items": { "type": "string" },
      "default": []
    },
    "allglobs": {
      "title": "allglobs",
      "description":
        "Prints access information about all globals, not just races.",
      "type": "boolean",
      "default": false
    },
    "kernel": {
      "title": "kernel",
      "description": "For analyzing Linux Device Drivers.",
      "type": "boolean",
      "default": false
    },
    "dump_globs": {
      "title": "dump_globs",
      "description": "Print out the global invariant.",
      "type": "boolean",
      "default": false
    },
    "result": {
      "title": "result",
      "description":
        "Result style: none, fast_xml, json, pretty, pretty-deterministic, json-messages, sarif, dashboard.",
      "type": "string",
      "enum": ["none", "fast_xml", "g2html", "xslt", "json", "pretty", "pretty-deterministic", "json-messages", "sarif", "dashboard"],
      "default": "none"
    },
    "solver": {
      "title": "solver",
      "description": "Picks the solver.",
      "type": "string",
      "default": "td3"
    },
    "comparesolver": {
      "title": "comparesolver",
      "description": "Picks another solver for comparison.",
      "type": "string",
      "default": ""
    },
    "allfuns": {
      "title": "allfuns",
      "description":
        "Analyzes all the functions (not just beginning from main). This requires exp.earlyglobs!",
      "type": "boolean",
      "default": false
    },
    "nonstatic": {
      "title": "nonstatic",
      "description": "Analyzes all non-static functions.",
      "type": "boolean",
      "default": false
    },
    "colors": {
      "title": "colors",
      "description":
        "Colored output (via ANSI escape codes). 'auto': enabled if stdout is a terminal (instead of a pipe); 'always', 'never'.",
      "type": "string",
      "enum": ["auto", "always", "never"],
      "default": "auto"
    },
    "save_run": {
      "title": "save_run",
      "description":
        "Save the result of the solver, the current configuration and meta-data about the run to this directory (if set). The data can then be loaded (without solving again) to do post-processing like generating output in a different format or comparing results.",
      "type": "string",
      "default": ""
    },
    "load_run": {
      "title": "load_run",
      "description": "Load a saved run. See save_run.",
      "type": "string",
      "default": ""
    },
    "compare_runs": {
      "title": "compare_runs",
      "description":
        "Load these saved runs and compare the results. Note that currently only two runs can be compared!",
      "type": "array",
      "items": { "type": "string" },
      "default": []
    },
    "warn_at": {
      "title": "warn_at",
      "description":
        "When to output warnings. Values: 'post' (default): after solving; 'never': no warnings; 'early': for debugging - outputs warnings already while solving (may lead to spurious warnings/asserts that would disappear after narrowing).",
      "type": "string",
      "enum": ["post", "never", "early"],
      "default": "post"
    },
    "gobview": {
      "title": "gobview",
      "description":
        "Include additional information for GobView (e.g., the Goblint warning messages) in the directory specified by 'save_run'.",
      "type": "boolean",
      "default": false
    },
    "jobs": {
      "title": "jobs",
      "description": "Maximum number of parallel jobs. If 0, then number of cores is used. Currently used for preprocessing and g2html.",
      "type": "integer",
      "default": 1
    },
    "goblint-dir": {
      "title": "goblint-dir",
      "description": "Directory used for intermediate data.",
      "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",
      "type": "object",
      "properties": {
        "enabled": {
          "title": "pre.enabled",
          "description": "Run the C preprocessor.",
          "type": "boolean",
          "default": true
        },
        "keep": {
          "title": "pre.keep",
          "description":
            "Keep the intermediate output of running the C preprocessor.",
          "type": "boolean",
          "default": false
        },
        "exist": {
          "title": "pre.exist",
          "description": "Use existing preprocessed files.",
          "type": "boolean",
          "default": false
        },
        "includes": {
          "title": "pre.includes",
          "description": "List of directories to include.",
          "type": "array",
          "items": { "type": "string" },
          "default": []
        },
        "kernel_includes": {
          "title": "pre.kernel_includes",
          "description": "List of kernel directories to include.",
          "type": "array",
          "items": { "type": "string" },
          "default": []
        },
        "custom_includes": {
          "title": "pre.custom_includes",
          "description": "List of custom directories to include.",
          "type": "array",
          "items": { "type": "string" },
          "default": []
        },
        "kernel-root": {
          "title": "pre.kernel-root",
          "description": "Root directory for Linux kernel (linux-headers)",
          "type": "string",
          "default": ""
        },
        "cppflags": {
          "title": "pre.cppflags",
          "description": "Pre-processing parameters.",
          "type": "array",
          "items": { "type": "string" },
          "default": []
        },
        "compdb": {
          "title": "pre.compdb",
          "type": "object",
          "properties": {
            "original-path": {
              "title": "pre.compdb.original-path",
              "description":
                "Original absolute path of Compilation Database. Used to reroot all absolute paths in there if moved, e.g. in container mounts.",
              "type": "string",
              "default": ""
            },
            "split": {
              "title": "pre.compdb.split",
              "description": "Split Compilation Database entries containing multiple .c files.",
              "type": "boolean",
              "default": false
            }
          },
          "additionalProperties": false
        },
        "transform-paths": {
          "title": "pre.transform-paths",
          "description": "Normalize and relativize paths in parsed CIL locations. Can cause issues locating YAML witness invariants due to differing paths.",
          "type": "boolean",
          "default": true
        }
      },
      "additionalProperties": false
    },
    "cil": {
      "title": "cil",
      "description": "CIL configuration",
      "type": "object",
      "properties": {
        "merge": {
          "title": "cil.merge",
          "type": "object",
          "properties": {
            "inlines": {
              "title": "cil.merge.inlines",
              "description": "Merge inline functions (by their body printout).",
              "type": "boolean",
              "default": true
            }
          },
          "additionalProperties": false
        },
        "gnu89inline": {
          "title": "cil.gnu89inline",
          "type": "boolean",
          "description": "Indicates whether gnu89 semantic should be used for inline functions.",
          "default": false
        },
        "addNestedScopeAttr": {
          "title": "cil.addNestedScopeAttr",
          "type": "boolean",
          "description": "Indicates whether variables that CIL pulls out of their scope should be marked.",
          "default": false
        }
      },
      "additionalProperties": false
    },
    "server": {
      "title": "Server",
      "description": "Server mode",
      "type": "object",
      "properties": {
        "enabled": {
          "title": "server.enabled",
          "description": "Enable server mode",
          "type": "boolean",
          "default": false
        },
        "mode": {
          "title": "server.mode",
          "description": "Server transport mode",
          "type": "string",
          "enum": ["stdio", "unix"],
          "default": "stdio"
        },
        "unix-socket": {
          "title": "server.unix-socket",
          "description": "The path to the UNIX socket",
          "type": "string",
          "default": "goblint.sock"
        },
        "reparse": {
          "title": "server.reparse",
          "description": "Reparse source files before each analysis run",
          "type": "boolean",
          "default": false
        }
      },
      "additionalProperties": false
    },
    "ana": {
      "title": "Analyses",
      "description": "Options for analyses",
      "type": "object",
      "properties": {
        "activated": {
          "title": "ana.activated",
          "description": "Lists of activated analyses.",
          "type": "array",
          "items": { "type": "string" },
          "default": [
            "expRelation", "base", "threadid", "threadflag", "threadreturn",
            "escape", "mutexEvents", "mutex", "access", "race", "mallocWrapper", "mhp",
            "assert", "pthreadMutexType"
          ]
        },
        "path_sens": {
          "title": "ana.path_sens",
          "description": "List of path-sensitive analyses",
          "type": "array",
          "items": { "type": "string" },
          "default": [ "mutex", "malloc_null", "uninit", "expsplit", "activeSetjmp", "memLeak", "branchSet"]
        },
        "ctx_insens": {
          "title": "ana.ctx_insens",
          "description": "List of context-insensitive analyses. This setting is ignored if `ana.ctx_sens` contains elements.",
          "type": "array",
          "items": { "type": "string" },
          "default": []
        },
        "ctx_sens": {
          "title": "ana.ctx_sens",
          "description": "List of context-sensitive analyses. In case this list is empty, `ana.ctx_insens` will be used to determine the set of context-insensitive analyses.",
          "type": "array",
          "items": { "type": "string" },
          "default": []
        },
        "setjmp" : {
          "title": "ana.setjmp",
          "description": "Setjmp/Longjmp analysis",
          "type": "object",
          "properties": {
            "split": {
              "title": "ana.setjmp.split",
              "description": "Split returns of setjmp",
              "type": "string",
              "enum": ["none", "coarse", "precise"],
              "default": "precise"
            }
          },
          "additionalProperties": false
        },
        "int": {
          "title": "ana.int",
          "type": "object",
          "properties": {
            "def_exc": {
              "title": "ana.int.def_exc",
              "description":
                "Use IntDomain.DefExc: definite value/exclusion set.",
              "type": "boolean",
              "default": true
            },
            "interval": {
              "title": "ana.int.interval",
              "description":
                "Use IntDomain.Interval32: (Z.t * Z.t) option.",
              "type": "boolean",
              "default": false
            },
            "interval_set": {
              "title": "ana.int.interval_set",
              "description": "Use IntDomain.IntervalSet: (Z.t * Z.t) list.",
              "type": "boolean",
              "default": false
            },
            "enums": {
              "title": "ana.int.enums",
              "description":
                "Use IntDomain.Enums: Inclusion/Exclusion sets. Go to top on arithmetic operations (except for some easy cases, e.g. multiplication with 0). Joins on widen, i.e. precise integers as long as not derived from arithmetic expressions.",
              "type": "boolean",
              "default": false
            },
            "bitfield": {
              "title": "ana.int.bitfield",
              "description":
                "Use IntDomain.Bitfield: Bitfield domain for integers.",
              "type": "boolean",
              "default": false
            },
            "congruence": {
              "title": "ana.int.congruence",
              "description":
                "Use IntDomain.Congruence: (c, m) option, meaning congruent to c modulo m",
              "type": "boolean",
              "default": false
            },
            "refinement": {
              "title": "ana.int.refinement",
              "description":
                "Use mutual refinement of integer domains. Either 'never', 'once' or 'fixpoint'. Counterintuitively, may reduce precision unless ana.int.interval_narrow_by_meet is also enabled.",
              "type": "string",
              "enum": ["never", "once", "fixpoint"],
              "default": "never"
            },
            "def_exc_widen_by_join": {
              "title": "ana.int.def_exc_widen_by_join",
              "description":
                "Perform def_exc widening by joins. Gives threshold-widening like behavior, with thresholds given by the ranges of different integer types.",
              "type": "boolean",
              "default": false
            },
            "interval_narrow_by_meet": {
              "title": "ana.int.interval_narrow_by_meet",
              "description": "Perform interval narrowing by meets. Avoids precision loss if intervals are refined by def_exc ranges, which are more precise than type range.",
              "type": "boolean",
              "default": false
            },
            "interval_threshold_widening": {
              "title": "ana.int.interval_threshold_widening",
              "description":
                "Use constants appearing in program as threshold for widening",
              "type": "boolean",
              "default": false
            },
            "interval_threshold_widening_constants": {
              "title": "ana.int.interval_threshold_widening_constants",
              "description":
                "Which constants in the program should be considered as threshold constants (all/comparisons)",
              "type": "string",
              "enum": ["all", "comparisons"],
              "default": "all"
            }
          },
          "additionalProperties": false
        },
        "float": {
          "title": "ana.float",
          "type": "object",
          "properties": {
            "interval": {
              "title": "ana.float.interval",
              "description":
                "Use FloatDomain: (float * float) option.",
              "type": "boolean",
              "default": false
            },
            "evaluate_math_functions": {
              "title": "ana.float.evaluate_math_functions",
              "description":
                "Allow a more precise evaluation of some functions from math.h. Evaluation of functions may differ depending on the implementation of math.h. Caution: For some implementations of functions it is not guaranteed that they behave monotonic where they mathematically should, thus possibly leading to unsoundness.",
              "type": "boolean",
              "default": false
            }
          },
          "additionalProperties": false
        },
        "pml": {
          "title": "ana.pml",
          "type": "object",
          "properties": {
            "debug": {
              "title": "ana.pml.debug",
              "description":
                "Insert extra assertions into Promela code for debugging.",
              "type": "boolean",
              "default": true
            }
          },
          "additionalProperties": false
        },
        "opt": {
          "title": "ana.opt",
          "type": "object",
          "properties": {
            "hashcons": {
              "title": "ana.opt.hashcons",
              "description":
                "Should we try to save memory and speed up equality by hashconsing?",
              "type": "boolean",
              "default": true
            },
            "hashcached": {
              "title": "ana.opt.hashcached",
              "description":
                "Should we try to save memory and speed up equality by caching hashes of contexts? This is useful when hashconsing is off",
              "type": "boolean",
              "default": false
            },
            "equal": {
              "title": "ana.opt.equal",
              "description":
                "First try physical equality (==) before {D,G,C}.equal (only done if hashcons is disabled since it basically does the same via its tags).",
              "type": "boolean",
              "default": true
            }
          },
          "additionalProperties": false
        },
        "autotune": {
          "title": "ana.autotune",
          "type": "object",
          "properties": {
            "enabled": {
              "title": "ana.autotune.enabled",
              "description": "Try to intelligently select analyses based on analysed file",
              "type": "boolean",
              "default": false
            },
            "activated": {
              "title": "ana.autotune.activated",
              "description": "Lists of activated tuning options.",
              "type": "array",
              "items": {
                "type": "string",
                "enum": [
                  "congruence",
                  "reduceAnalyses",
                  "mallocWrappers",
                  "noRecursiveIntervals",
                  "enums",
                  "loopUnrollHeuristic",
                  "forceLoopUnrollForFewLoops",
                  "arrayDomain",
                  "octagon",
                  "wideningThresholds",
                  "memsafetySpecification",
                  "concurrencySafetySpecification",
                  "noOverflows",
                  "termination",
                  "tmpSpecialAnalysis"
                ]
              },
              "default": [
                "congruence",
                "reduceAnalyses",
                "mallocWrappers",
                "noRecursiveIntervals",
                "enums",
                "loopUnrollHeuristic",
                "arrayDomain",
                "octagon",
                "wideningThresholds",
                "memsafetySpecification",
                "concurrencySafetySpecification",
                "noOverflows",
                "termination",
                "tmpSpecialAnalysis"
              ]
            }
          },
          "additionalProperties": false
        },
        "sv-comp": {
          "title": "ana.sv-comp",
          "type": "object",
          "properties": {
            "enabled": {
              "title": "ana.sv-comp.enabled",
              "description": "SV-COMP mode",
              "type": "boolean",
              "default": false
            },
            "functions": {
              "title": "ana.sv-comp.functions",
              "description": "Handle SV-COMP __VERIFIER* functions",
              "type": "boolean",
              "default": false
            }
          },
          "additionalProperties": false
        },
        "specification": {
          "title": "ana.specification",
          "description": "SV-COMP specification (path or string)",
          "type": "string",
          "default": ""
        },
        "wp": {
          "title": "ana.wp",
          "description":
            "Weakest precondition feasibility analysis for SV-COMP violations",
          "type": "boolean",
          "default": false
        },
        "arrayoob": {
          "title": "ana.arrayoob",
          "description": "Array out of bounds check",
          "type": "boolean",
          "default": false
        },
        "base": {
          "title": "ana.base",
          "type": "object",
          "properties": {
            "context": {
              "title": "ana.base.context",
              "type": "object",
              "properties": {
                "non-ptr": {
                  "title": "ana.base.context.non-ptr",
                  "description": "Non-address values in function contexts.",
                  "type": "boolean",
                  "default": true
                },
                "int": {
                  "title": "ana.base.context.int",
                  "description": "Integer values in function contexts.",
                  "type": "boolean",
                  "default": true
                },
                "interval": {
                  "title": "ana.base.context.interval",
                  "description":
                    "Integer values of the Interval domain in function contexts.",
                  "type": "boolean",
                  "default": true
                },
                "interval_set": {
                  "title": "ana.base.context.interval_set",
                  "description":
                    "Integer values of the IntervalSet domain in function contexts.",
                  "type": "boolean",
                  "default": true
                },
                "bitfield": {
                  "title": "ana.base.context.bitfield",
                  "description": "Bitfield values in function contexts.",
                  "type": "boolean",
                  "default": true
                }
              },
              "additionalProperties": false
            },
            "strings": {
              "title": "ana.base.strings",
              "type": "object",
              "properties": {
                "domain": {
                  "title": "ana.base.strings.domain",
                  "description": "Domain for string literals.",
                  "type": "string",
                  "enum": ["unit", "flat", "disjoint"],
                  "default": "flat"
                }
              },
              "additionalProperties": false
            },
            "partition-arrays": {
              "title": "ana.base.partition-arrays",
              "type": "object",
              "properties": {
                "keep-expr": {
                  "title": "ana.base.partition-arrays.keep-expr",
                  "description":
                    "When using the partitioning which expression should be used for partitioning ('first', 'last')",
                  "type": "string",
                  "enum": ["first", "last"],
                  "default": "first"
                },
                "partition-by-const-on-return": {
                  "title": "ana.base.partition-arrays.partition-by-const-on-return",
                  "description":
                    "When using the partitioning should arrays be considered partitioned according to a constant if a var in the expression used for partitioning goes out of scope?",
                  "type": "boolean",
                  "default": false
                },
                "smart-join": {
                  "title": "ana.base.partition-arrays.smart-join",
                  "description":
                    "When using the partitioning should the join of two arrays partitioned according to different expressions be partitioned as well if possible? If keep-expr is 'last' this behavior is enabled regardless of the flag value. Caution: Not always advantageous.",
                  "type": "boolean",
                  "default": false
                }
              },
              "additionalProperties": false
            },
            "arrays":{
              "title": "ana.base.arrays",
              "type": "object",
              "properties": {
                "domain": {
                  "title": "ana.base.arrays.domain",
                  "description":
                    "The domain that should be used for arrays. When employing the partition array domain, make sure to enable the expRelation analysis as well. When employing the unrolling array domain, make sure to set the ana.base.arrays.unrolling-factor >0.",
                  "type": "string",
                  "enum": ["trivial", "partitioned", "unroll"],
                  "default": "trivial"
                },
                "unrolling-factor": {
                  "title": "ana.base.arrays.unrolling-factor",
                  "description": "Indicates how many values will the unrolled part of the unrolled array domain contain.",
                  "type": "integer",
                  "default": 0
                },
                "nullbytes": {
                  "title": "ana.base.arrays.nullbytes",
                  "description": "Whether the Null Byte array domain should be activated.",
                  "type": "boolean",
                  "default": false
                }
              },
              "additionalProperties": false
            },
            "structs": {
              "title": "ana.base.structs",
              "type": "object",
              "properties": {
                "domain": {
                  "title": "ana.base.structs.domain",
                  "description":
                    "The domain that should be used for structs. simple/sets/keyed/combined-all/combined-sk",
                  "type": "string",
                  "enum": ["simple", "sets", "keyed", "combined-all", "combined-sk"],
                  "default": "simple"
                },
                "key": {
                  "title": "ana.base.structs.key",
                  "type": "object",
                  "properties": {
                    "forward": {
                      "title": "ana.base.structs.key.forward",
                      "description":
                        "Whether the struct key should be picked going from first field to last.",
                      "type": "boolean",
                      "default": true
                    },
                    "avoid-ints": {
                      "title": "ana.base.structs.key.avoid-ints",
                      "description":
                        "Whether integers should be avoided for key.",
                      "type": "boolean",
                      "default": true
                    },
                    "prefer-ptrs": {
                      "title": "ana.base.structs.key.prefer-ptrs",
                      "description":
                        "Whether pointers should be preferred for key.",
                      "type": "boolean",
                      "default": true
                    }
                  },
                  "additionalProperties": false
                }
              },
              "additionalProperties": false
            },
            "privatization": {
              "title": "ana.base.privatization",
              "description":
                "Which privatization to use? none/vojdani/mutex-oplus/mutex-meet/mutex-meet-tid/protection/protection-read/mine/mine-nothread/mine-W/mine-W-noinit/lock/lock-tid/write/write-tid/write+lock/write+lock-tid",
              "type": "string",
              "enum": ["none", "vojdani", "mutex-oplus", "mutex-meet", "protection", "protection-tid", "protection-atomic", "protection-read", "protection-read-tid", "protection-read-atomic", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "lock-tid", "write", "write-tid", "write+lock", "write+lock-tid", "mutex-meet-tid"],
              "default": "protection-read"
            },
            "priv": {
              "title": "ana.base.priv",
              "type": "object",
              "properties": {
                "protection": {
                  "title": "ana.base.priv.protection",
                  "description": "Options for protection based privatization schemes.",
                  "type": "object",
                  "properties": {
                    "changes-only": {
                      "title": "ana.base.priv.protection.changes-only",
                      "description": "Only propagate changes to globals on unlock, don't side the full value of the privatized global.",
                      "type": "boolean",
                      "default": false
                    }
                  },
                  "additionalProperties": false
                },
                "not-started": {
                  "title": "ana.base.priv.not-started",
                  "description":
                    "Exclude writes from threads that may not be started yet",
                  "type": "boolean",
                  "default": true
                },
                "must-joined": {
                  "title": "ana.base.priv.must-joined",
                  "description":
                    "Exclude writes from threads that must have been joined",
                  "type": "boolean",
                  "default": true
                }
              },
              "additionalProperties": false
            },
            "invariant": {
              "title": "ana.base.invariant",
              "type": "object",
              "properties": {
                "enabled": {
                  "title": "ana.base.invariant.enabled",
                  "description": "Generate base analysis invariants",
                  "type": "boolean",
                  "default": true
                },
                "local": {
                  "title": "ana.base.invariant.local",
                  "description": "Keep local variables in invariants",
                  "type": "boolean",
                  "default": true
                },
                "global": {
                  "title": "ana.base.invariant.global",
                  "description": "Keep global variables in invariants",
                  "type": "boolean",
                  "default": true
                },
                "blobs": {
                  "title": "ana.base.invariant.blobs",
                  "description": "Whether to dump assertions about all blobs. Enabling this option may lead to unsound asserts.",
                  "type": "boolean",
                  "default": false
                },
                "unassume": {
                  "title": "ana.base.invariant.unassume",
                  "description": "How many times to unassume an invariant: once or until fixpoint (at least twice as expensive).",
                  "type": "string",
                  "enum": ["once", "fixpoint"],
                  "default": "once"
                },
                "int": {
                  "title": "ana.base.invariant.int",
                  "type": "object",
                  "properties": {
                    "simplify": {
                      "title": "ana.base.invariant.int.simplify",
                      "description": "How much to simplify int domain invariants. Value \"int\" only simplifies definite integers. Without int domain refinement \"all\" might not be maximally precise.",
                      "type": "string",
                      "enum": ["none", "int", "all"],
                      "default": "all"
                    }
                  },
                  "additionalProperties": false
                }
              },
              "additionalProperties": false
            },
            "eval": {
              "title": "ana.base.eval",
              "type": "object",
              "properties": {
                "deep-query": {
                  "title": "ana.base.eval.deep-query",
                  "description": "Perform EvalInt queries on all subexpressions, not just the outermost expression.",
                  "type": "boolean",
                  "default": true
                }
              },
              "additionalProperties": false
            },
            "branch": {
              "title": "ana.base.branch",
              "type": "object",
              "properties": {
                "refine-pointer-by-pointee": {
                  "title": "ana.base.branch.refine-pointer-by-pointee",
                  "description": "Refine points-to sets by dereferenced value when branching.",
                  "type": "boolean",
                  "default": true
                }
              },
              "additionalProperties": false
            }
          },
          "additionalProperties": false
        },
        "malloc": {
          "title": "ana.malloc",
          "type": "object",
          "properties": {
            "wrappers": {
              "title": "ana.malloc.wrappers",
              "description":
                "Loads a list of known malloc wrapper functions.",
              "type": "array",
              "items": { "type": "string" },
              "default": [
                "kmalloc", "__kmalloc", "usb_alloc_urb", "__builtin_alloca",
                "kzalloc"
              ]
            },
            "unique_address_count": {
                "title": "ana.malloc.unique_address_count",
                "description": "Number of unique memory addresses allocated for each malloc node.",
                "type": "integer",
                "default": 0
            }
          },
          "additionalProperties": false
        },
        "apron": {
          "title": "ana.apron",
          "type": "object",
          "properties": {
            "strengthening": {
              "title": "ana.apron.strengthening",
              "description": "Apply strengthening in join for extra precision with heterogeneous environments. Expensive!",
              "type": "boolean",
              "default": false
            },
            "domain": {
              "title": "ana.apron.domain",
              "description":
                "Which domain should be used for the Apron analysis. Can be 'octagon', 'interval' or 'polyhedra'",
              "type": "string",
              "enum": ["octagon", "interval", "polyhedra", "affeq"],
              "default": "octagon"
            },
            "threshold_widening": {
              "title": "ana.apron.threshold_widening",
              "description":
                "Use constants appearing in program as threshold for widening",
              "type": "boolean",
              "default": false
            },
            "threshold_widening_constants": {
              "title": "ana.apron.threshold_widening_constants",
              "description":
                "Which constants in the programm should be considered as threshold constants",
              "type": "string",
              "enum": ["all", "comparisons"],
              "default": "all"
            },
            "invariant": {
              "title": "ana.apron.invariant",
              "type": "object",
              "properties": {
                "diff-box": {
                  "title": "ana.apron.invariant.diff-box",
                  "description": "Only generate truly relational invariants by subtracting non-relational box invariants",
                  "type": "boolean",
                  "default": false
                }
              },
              "additionalProperties": false
            }
          },
          "additionalProperties": false
        },
        "relation": {
          "title": "ana.relation",
          "type": "object",
          "properties": {
            "context": {
              "title": "ana.relation.context",
              "description": "Entire relation in function contexts.",
              "type": "boolean",
              "default": true
            },
            "privatization": {
              "title": "ana.relation.privatization",
              "description":
                "Which relation privatization to use? top/protection/protection-path/mutex-meet/mutex-meet-tid/mutex-meet-tid-cluster12/mutex-meet-tid-cluster2/mutex-meet-tid-cluster-max/mutex-meet-tid-cluster-power",
              "type": "string",
              "enum": ["top", "protection", "protection-path", "mutex-meet", "mutex-meet-atomic", "mutex-meet-tid", "mutex-meet-tid-atomic", "mutex-meet-tid-cluster12", "mutex-meet-tid-cluster2", "mutex-meet-tid-cluster-max", "mutex-meet-tid-cluster-power"],
              "default": "mutex-meet"
            },
            "priv": {
              "title": "ana.relation.priv",
              "type": "object",
              "properties": {
                "not-started": {
                  "title": "ana.relation.priv.not-started",
                  "description":
                    "Exclude writes from threads that may not be started yet",
                  "type": "boolean",
                  "default": true
                },
                "must-joined": {
                  "title": "ana.relation.priv.must-joined",
                  "description":
                    "Exclude writes from threads that must have been joined",
                  "type": "boolean",
                  "default": true
                }
              },
              "additionalProperties": false
            },
            "invariant": {
              "title": "ana.relation.invariant",
              "type": "object",
              "properties": {
                "one-var": {
                  "title": "ana.relation.invariant.one-var",
                  "description": "Generate invariants with only one variable",
                  "type": "boolean",
                  "default": false
                },
                "local": {
                  "title": "ana.relation.invariant.local",
                  "description": "Keep local variables in invariants",
                  "type": "boolean",
                  "default": true
                },
                "global": {
                  "title": "ana.relation.invariant.global",
                  "description": "Keep global variables in invariants",
                  "type": "boolean",
                  "default": true
                }
              },
              "additionalProperties": false
            }
          },
          "additionalProperties": false
        },
        "context": {
          "title": "ana.context",
          "type": "object",
          "properties": {
            "widen": {
              "title": "ana.context.widen",
              "description":
                "Do widening on contexts. Keeps a map of function to call state; enter will then return the widened local state for recursive calls.",
              "type": "boolean",
              "default": false
            },
            "gas_value": {
              "title": "ana.context.gas_value",
              "description": "Denotes the gas value x for the ContextGasLifter. Negative values deactivate the context gas, zero yields a context-insensitive analysis. If enabled, the first x recursive calls of the call stack are analyzed context-sensitively. Any calls deeper in the call stack are analyzed with the same (empty) context.",
              "type": "integer",
              "default": -1
            },
            "gas_scope": {
              "title": "ana.context.gas_scope",
              "description":
                "Whether the gas should be  'global' (default) or per 'function'",
              "type": "string",
              "enum": ["global","function"],
              "default": "global"
            },
            "callString_length": {
              "title": "ana.context.callString_length",
              "description": "Length of the call string that should be used as context for the call_string and/or call_site analyses. In case the value is zero, the analysis is context-insensitive. For a negative value, an infinite call string is used! For this option to have an effect, one of the analyses in `callstring.ml` must be activated.",
              "type": "integer",
              "default": 2
            }
          },
          "additionalProperties": false
        },
        "thread": {
          "title": "ana.thread",
          "type": "object",
          "properties": {
            "domain": {
              "title": "ana.thread.domain",
              "description":
                "Which domain should be used for the thread ids. Can be 'history' or 'plain'",
              "type": "string",
              "enum": ["history", "plain"],
              "default": "history"
            },
            "include-node" : {
              "title": "ana.thread.include-node",
              "description":
                "Whether the node at which a thread is created is part of its threadid",
              "type": "boolean",
              "default" : true
            },
            "wrappers": {
              "title": "ana.thread.wrappers",
              "description":
                "Loads a list of known thread spawn (pthread_create) wrapper functions.",
              "type": "array",
              "items": { "type": "string" },
              "default": []
            },
            "unique_thread_id_count": {
              "title": "ana.thread.unique_thread_id_count",
              "description": "Number of unique thread IDs allocated for each pthread_create node.",
              "type": "integer",
              "default": 0
            },
            "context": {
              "title": "ana.thread.context",
              "type": "object",
              "properties": {
                "create-edges": {
                  "title": "ana.thread.context.create-edges",
                  "description": "threadID analysis: Encountered create edges in context.",
                  "type": "boolean",
                  "default": true
                }
              },
              "additionalProperties": false
            }
          },
          "additionalProperties": false
        },
        "race": {
          "title": "ana.race",
          "type": "object",
          "properties": {
            "free": {
              "title": "ana.race.free",
              "description": "Consider memory free as racing write.",
              "type": "boolean",
              "default": true
            },
            "call": {
              "title": "ana.race.call",
              "description": "Report races for thread-unsafe function calls.",
              "type": "boolean",
              "default": true
            },
            "direct-arithmetic": {
              "title": "ana.race.direct-arithmetic",
              "description": "Collect and distribute direct (i.e. not in a field) accesses to arithmetic types.",
              "type": "boolean",
              "default": false
            },
            "volatile" :{
              "title": "ana.race.volatile",
              "description": "Report races for volatile variables.",
              "type": "boolean",
              "default": true
            }
          },
          "additionalProperties": false
        },
        "dead-code" : {
          "title": "ana.dead-code",
          "type": "object",
          "properties": {
            "lines": {
              "title": "ana.dead-code.lines",
              "description": "Print information about lines of dead code.",
              "type": "boolean",
              "default": true
            },
            "branches": {
              "title": "ana.dead-code.branches",
              "description": "Print information about dead branches.",
              "type": "boolean",
              "default": true
            },
            "functions": {
              "title": "ana.dead-code.functions",
              "description": "Print information about dead (uncalled) functions.",
              "type": "boolean",
              "default": true
            }
          },
          "additionalProperties": false
        },
        "extract-pthread" : {
          "title": "ana.extract-pthread",
          "type": "object",
          "properties": {
            "assume_success": {
              "title": "ana.extract-pthread.assume_success",
              "description": "Assume that all POSIX pthread functions succeed.",
              "type": "boolean",
              "default": true
            },
            "ignore_assign": {
              "title": "ana.extract-pthread.ignore_assign",
              "description": "Ignores any assigns in POSIX programs.",
              "type": "boolean",
              "default": true
            }
          },
          "additionalProperties": false
        },
        "widen": {
          "title": "ana.widen",
          "type": "object",
          "properties": {
            "tokens": {
              "title": "ana.widen.tokens",
              "description": "Delay widenings using widening tokens.",
              "type": "boolean",
              "default": false
            },
            "delay": {
              "title": "ana.widen.delay",
              "type": "object",
              "properties": {
                "local": {
                  "title": "ana.widen.delay.local",
                  "description": "Delay local constraint unknown widenings by count.",
                  "type": "integer",
                  "default": 0
                },
                "global": {
                  "title": "ana.widen.delay.global",
                  "description": "Delay global constraint unknown widenings by count.",
                  "type": "integer",
                  "default": 0
                }
              },
              "additionalProperties": false
            }
          },
          "additionalProperties": false
        },
        "c2po": {
          "title": "ana.c2po",
          "type": "object",
          "properties": {
            "askbase": {
              "title": "ana.c2po.askbase",
              "description": "If true, the C-2PO Analysis uses the MayPointTo query to infer additional disequalities.",
              "type": "boolean",
              "default": true
            },
            "join_algorithm": {
              "title": "ana.c2po.join_algorithm",
              "description": "Which join algorithm 'c2po' should use. Values: 'partition' (default): the more efficient version, it uses only the partition to compute the join. Circular equalities are lost during the join; 'precise': a more precise version, uses the automaton to compute the join.",
              "type": "string",
              "enum": [
                "precise",
                "partition"
              ],
              "default": "partition"
            },
            "equal": {
              "title": "ana.c2po.equal",
              "description": "Which equal algorithm 'c2po' should use. Values: 'partition' (default): it compares the partitions each time; 'normal_form': computes a normal form of the domain to compare them. It is lazily computed. The two possibilities are equivalent in precision, but in some cases computing the normal form is more efficient, as it is computed only once per distinct domain element.",
              "type": "string",
              "enum": [
                "normal_form",
                "partition"
              ],
              "default": "partition"
            }
          },
          "additionalProperties": false
        },
        "unassume": {
          "title": "ana.unassume",
          "type": "object",
          "properties": {
            "precheck": {
              "title": "ana.unassume.precheck",
              "description": "Check if invariant contradicts reached state before unassuming.",
              "type": "boolean",
              "default": false
            }
          },
          "additionalProperties": false
        },
        "var_eq": {
          "title": "ana.var_eq",
          "type": "object",
          "properties": {
            "invariant": {
              "title": "ana.var_eq.invariant",
              "type": "object",
              "properties": {
                "enabled": {
                  "title": "ana.var_eq.invariant.enabled",
                  "description": "Generate var_eq analysis invariants",
                  "type": "boolean",
                  "default": true
                }
              },
              "additionalProperties": false
            }
          },
          "additionalProperties": false
        },
        "affeq": {
          "title": "ana.affeq",
          "type": "object",
          "properties": {
            "sparse": {
              "title": "ana.affeq.sparse",
              "description": "Use sparse implementation of Affine Equality analysis (using lists). If set to false, the dense version is used (using arrays). Default is true (sparse implementation)",
              "type": "boolean",
              "default": true
            }
          },
          "additionalProperties": false
        }
      },
      "additionalProperties": false
    },
    "incremental": {
      "title": "Incremental",
      "description": "Incremental analysis options",
      "type": "object",
      "properties": {
        "load": {
          "title": "incremental.load",
          "description":
            "Load incremental analysis results, in case any exist.",
          "type": "boolean",
          "default": false
        },
        "load-dir": {
          "title": "incremental.load-dir",
          "description": "Location where to load incremental analysis results from.",
          "type": "string",
          "default": "incremental_data"
        },
        "only-rename": {
          "title": "incremental.only-rename",
          "description":
            "Only reset IDs of unchanged objects in the AST. Do  not reuse solver results. This option is mainly useful for benchmarking purposes.",
          "type": "boolean",
          "default": false
        },
        "save": {
          "title": "incremental.save",
          "description": "Store incremental analysis results.",
          "type": "boolean",
          "default": false
        },
        "save-dir": {
          "title": "incremental.save-dir",
          "description": "Location where to save incremental analysis results to.",
          "type": "string",
          "default": "incremental_data"
        },
        "stable": {
          "title": "incremental.stable",
          "description":
            "Reuse the stable set and selectively destabilize it (recommended).",
          "type": "boolean",
          "default": true
        },
        "wpoint": {
          "title": "incremental.wpoint",
          "description":
            "Reuse the wpoint set (not recommended). Reusing the wpoint will combine existing results at previous widening points.",
          "type": "boolean",
          "default": false
        },
        "reluctant": {
          "title": "incremental.reluctant",
          "type": "object",
          "properties": {
            "enabled": {
              "title": "incremental.reluctant.enabled",
              "description":
                "Destabilize nodes in changed functions reluctantly",
              "type": "boolean",
              "default": false
            }
          },
          "additionalProperties": false
        },
        "compare": {
          "title": "incremental.compare",
          "description":
            "Which comparison should be used for functions? 'ast'/'cfg' (cfg comparison also differentiates which nodes of a function have changed)",
          "type": "string",
          "enum": ["ast", "cfg"],
          "default": "ast"
        },
        "detect-renames": {
          "title": "incremental.detect-renames",
          "description": "If Goblint should try to detect renamed local variables, function parameters, functions and global variables",
          "type":"boolean",
          "default": true
        },
        "force-reanalyze": {
          "title": "incremental.force-reanalyze",
          "type": "object",
          "properties": {
            "funs": {
              "title": "incremental.force-reanalyze.funs",
              "description":
                "List of functions that are to be re-analayzed from scratch",
              "type": "array",
              "items": {
                "type": "string"
              },
              "default": []
            }
          },
          "additionalProperties": false
        },
        "restart": {
          "title": "incremental.restart",
          "type": "object",
          "properties": {
            "sided": {
              "title": "incremental.restart.sided",
              "type": "object",
              "properties": {
                "enabled": {
                  "title": "incremental.restart.sided.enabled",
                  "description": "Restart affected side-effected variables (transitively) to bot.",
                  "type": "boolean",
                  "default": false
                },
                "vars": {
                  "title": "incremental.restart.sided.vars",
                  "description": "Side-effected variables to restart. Globals are non-function entry nodes. Write-only is a subset of globals.",
                  "type": "string",
                  "enum": ["all", "global", "write-only"],
                  "default": "all"
                },
                "fuel": {
                  "title": "incremental.restart.sided.fuel",
                  "description": "Initial fuel for bounding transitive restarting, which uses one fuel each time when following side_fuel to restart. Zero fuel never restarts. Negative fuel doesn't bound (infinite fuel).",
                  "type": "integer",
                  "default": -1
                },
                "fuel-only-global": {
                  "title": "incremental.restart.sided.fuel-only-global",
                  "description": "Decrease fuel only when going to constraint system globals (not function entry nodes).",
                  "type": "boolean",
                  "default": false
                }
              },
              "additionalProperties": false
            },
            "list": {
              "title": "incremental.restart.list",
              "description": "List of globals variables and function definitions for which the analysis is to be restarted.",
              "type": "array",
              "items": {
                "type": "string"
              },
              "default": []
            },
            "write-only": {
              "title": "incremental.restart.write-only",
              "description": "Restart write-only variables to bot during postprocessing.",
              "type": "boolean",
              "default": true
            }
          },
          "additionalProperties": false
        },
        "postsolver": {
          "title": "incremental.postsolver",
          "type" : "object",
          "properties": {
            "enabled": {
              "title": "incremental.postsolver.enabled",
              "description": "Use incremental postsolver",
              "type": "boolean",
              "default": true
            },
            "superstable-reached" : {
              "title":  "incremental.postsolver.superstable-reached",
              "description": "Consider superstable set reached, may be faster but can lead to spurious warnings",
              "type": "boolean",
              "default": false
            }
          },
          "additionalProperties": false
        }
      },
      "additionalProperties": false
    },
    "lib": {
      "title": "Library functions",
      "description": "Options for library functions",
      "type": "object",
      "properties": {
        "activated": {
          "title": "lib.activated",
          "description": "List of activated libraries.",
          "type": "array",
          "items": {
            "type": "string",
            "enum": [
              "c",
              "posix",
              "pthread",
              "gcc",
              "glibc",
              "linux-userspace",
              "linux-kernel",
              "goblint",
              "sv-comp",
              "klever",
              "ncurses",
              "zstd",
              "pcre",
              "zlib",
              "liblzma",
              "legacy"
            ]
          },
          "default": [
            "c",
            "posix",
            "pthread",
            "gcc",
            "glibc",
            "linux-userspace",
            "goblint",
            "ncurses",
            "legacy"
          ]
        }
      },
      "additionalProperties": false
    },
    "sem": {
      "title": "Semantics",
      "description": "Options for semantics",
      "type": "object",
      "properties": {
        "unknown_function": {
          "title": "sem.unknown_function",
          "type": "object",
          "properties": {
            "spawn": {
              "title": "sem.unknown_function.spawn",
              "description":
                "Unknown function call spawns reachable functions",
              "type": "boolean",
              "default": true
            },
            "call": {
              "title": "sem.unknown_function.call",
              "description":
                "Unknown function call calls reachable functions",
              "type": "boolean",
              "default": true
            },
            "invalidate": {
              "title": "sem.unknown_function.invalidate",
              "type": "object",
              "properties": {
                "globals": {
                  "title": "sem.unknown_function.invalidate.globals",
                  "description":
                    "Unknown function call invalidates all globals",
                  "type": "boolean",
                  "default": true
                },
                "args": {
                  "title": "sem.unknown_function.invalidate.args",
                  "description":
                    "Unknown function call invalidates arguments passed to it",
                  "type": "boolean",
                  "default": true
                }
              },
              "additionalProperties": false
            },
            "read": {
              "title": "sem.unknown_function.read",
              "type": "object",
              "properties": {
                "args": {
                  "title": "sem.unknown_function.read.args",
                  "description":
                    "Unknown function call reads arguments passed to it",
                  "type": "boolean",
                  "default": true
                }
              },
              "additionalProperties": false
            }
          },
          "additionalProperties": false
        },
        "builtin_unreachable": {
          "title": "sem.builtin_unreachable",
          "type": "object",
          "properties": {
            "dead_code": {
              "title": "sem.builtin_unreachable.dead_code",
              "description":
                "__builtin_unreachable is assumed to be dead code",
              "type": "boolean",
              "default": false
            }
          },
          "additionalProperties": false
        },
        "noreturn": {
          "title": "sem.noreturn",
          "description": "Handling of C11 _Noreturn function specifier.",
          "type": "object",
          "properties": {
            "dead_code": {
              "title": "sem.noreturn.dead_code",
              "description":
                "For the purposes of detecting dead code, assume that functions marked noreturn don't return.",
              "type": "boolean",
              "default": false
            }
          },
          "additionalProperties": false
        },
        "int": {
          "title": "sem.int",
          "type": "object",
          "properties": {
            "signed_overflow": {
              "title": "sem.int.signed_overflow",
              "description":
                "How to handle overflows of signed types. Values: 'assume_top' (default): Assume signed overflow results in a top value; 'assume_none': Assume program is free of signed overflows;  'assume_wraparound': Assume signed types wrap-around and two's complement representation of signed integers",
              "type": "string",
              "enum": ["assume_top", "assume_none", "assume_wraparound"],
              "default": "assume_top"
            }
          },
          "additionalProperties": false
        },
        "null-pointer": {
          "title": "sem.null-pointer",
          "type": "object",
          "properties": {
            "dereference": {
              "title": "sem.null-pointer.dereference",
              "description": "NULL pointer dereference handling. assume_top: assume it results in a top value, assume_none: assume it doesn't happen",
              "type": "string",
              "enum": ["assume_top", "assume_none"],
              "default": "assume_none"
            }
          },
          "additionalProperties": false
        },
        "malloc": {
          "title": "sem.malloc",
          "type": "object",
          "properties": {
            "fail": {
              "title": "sem.malloc.fail",
              "description":
                "Consider the case where malloc or calloc fails when called with an argument other than zero. For the case of zero, see `sem.malloc.zero`.",
              "type": "boolean",
              "default": false
            },
            "zero": {
              "title": "sem.malloc.zero",
              "description": "What happens when allocating zero bytes? 'null': Return null pointer, 'pointer': Return a pointer to valid memory of size 0, 'either': Consider both cases.",
              "type": "string",
              "enum": ["null", "pointer","either"],
              "default": "either"
            }
          },
          "additionalProperties": false
        },
        "lock": {
          "title": "sem.lock",
          "type": "object",
          "properties": {
            "fail": {
              "title": "sem.lock.fail",
              "description":
                "Takes the possible failing of locking operations into account.",
              "type": "boolean",
              "default": false
            }
          },
          "additionalProperties": false
        },
        "assert": {
          "title": "sem.assert",
          "type": "object",
          "properties": {
            "refine": {
              "title": "sem.assert.refine",
              "description": "Standard assert refines state",
              "type": "boolean",
              "default": true
            }
          },
          "additionalProperties": false
        },
        "atexit": {
          "title": "sem.atexit",
          "type": "object",
          "properties": {
            "ignore": {
              "title": "sem.atexit.ignore",
              "description": "Ignore atexit callbacks (unsound).",
              "type": "boolean",
              "default": false
            }
          },
          "additionalProperties": false
        }
      },
      "additionalProperties": false
    },
    "trans": {
      "title": "Transformations",
      "description": "Options for transformations",
      "type": "object",
      "properties": {
        "activated": {
          "title": "trans.activated",
          "description":
            "Lists of activated transformations. Transformations happen after analyses.",
          "type": "array",
          "items": {
            "type": "string",
            "enum": ["partial", "expeval", "assert", "remove_dead_code"]
          },
          "default": []
        },
        "expeval": {
          "title": "trans.expeval",
          "type": "object",
          "properties": {
            "query_file_name": {
              "title": "trans.expeval.query_file_name",
              "description":
                "Path to the JSON file containing an expression evaluation query.",
              "type": "string",
              "default": ""
            }
          },
          "additionalProperties": false
        },
        "output" : {
          "title": "trans.output",
          "description": "Output filename for transformations that output a transformed file.",
          "type":"string",
          "default": "transformed.c"
        },
        "assert" : {
          "title": "trans.assert",
          "type": "object",
          "properties": {
            "function": {
              "title": "trans.assert.function",
              "description": "Function to use for assertions in output.",
              "type": "string",
              "enum": ["assert", "__goblint_check", "__VERIFIER_assert"],
              "default": "__VERIFIER_assert"
            },
            "wrap-atomic": {
              "title": "trans.assert.wrap-atomic",
              "description": "Wrap assertions in __VERIFIER_atomic_begin and __VERIFIER_atomic_end.",
              "type": "boolean",
              "default": true
            }
          },
          "additionalProperties": false
        }
      },
      "additionalProperties": false
    },
    "annotation": {
      "title": "Annotation",
      "description": "Options for annotations",
      "type": "object",
      "properties": {
        "int": {
          "title": "annotation.int",
          "type": "object",
          "properties": {
            "enabled": {
              "title": "annotation.int.enabled",
              "description":
                "Enable manual annotation of functions with desired precision, i.e., the activated IntDomains.",
              "type": "boolean",
              "default": false
            },
            "privglobs": {
              "title": "annotation.int.privglobs",
              "description":
                "Enables handling of privatized globals, by setting the precision to the heighest value, when annotation.int.enabled is true.",
              "type": "boolean",
              "default": true
            }
          },
          "additionalProperties": false
        },
        "float": {
          "title": "annotation.float",
          "type": "object",
          "properties": {
            "enabled": {
              "title": "annotation.float.enabled",
              "description":
                "Enable manual annotation of functions with desired precision, i.e., the activated FloatDomains.",
              "type": "boolean",
              "default": false
            }
          },
          "additionalProperties": false
        },
        "goblint_context": {
          "title": "annotation.goblint_context",
          "type": "object",
          "additionalProperties": {
            "type": "array",
            "items": {
              "type": "string",
              "enum": ["base.no-non-ptr", "base.non-ptr", "base.no-int", "base.int", "base.no-interval", "base.no-interval_set", "base.no-bitfield", "base.interval", "base.interval_set", "base.bitfield", "relation.no-context", "relation.context", "no-widen", "widen"]
            },
            "default": []
          }
        },
        "goblint_precision": {
          "title": "annotation.goblint_precision",
          "type": "object",
          "additionalProperties": {
            "type": "array",
            "items": {
              "type": "string",
              "enum": ["no-def_exc", "def_exc", "no-interval", "interval", "no-enums", "enums", "no-congruence", "congruence"]
            },
            "default": []
          }
        },
        "goblint_array_domain": {
          "title": "annotation.goblint_array_domain",
          "description": "Enable manual annotation of arrays with desired domain",
          "type": "boolean",
          "default": false
        },
        "goblint_relation_track": {
          "title": "annotation.goblint_relation_track",
          "description": "Let relation track variables only if they have the attribute goblint_relation_track",
          "type": "boolean",
          "default": false
        }
      },
      "additionalProperties": false
    },
    "exp": {
      "title": "Experimental",
      "description": "Experimental features",
      "type": "object",
      "properties": {
        "priv-prec-dump": {
          "title": "exp.priv-prec-dump",
          "description": "File to dump privatization precision data to.",
          "type": "string",
          "default": ""
        },
        "priv-distr-init": {
          "title": "exp.priv-distr-init",
          "description":
            "Distribute global initializations to all global invariants for more consistent widening dynamics.",
          "type": "boolean",
          "default": false
        },
        "relation": {
          "title": "exp.relation",
          "type": "object",
          "properties": {
            "prec-dump": {
              "title": "exp.relation.prec-dump",
              "description": "File to dump relation precision data to.",
              "type": "string",
              "default": ""
            }
          },
          "additionalProperties": false
        },
        "cfgdot": {
          "title": "exp.cfgdot",
          "description": "Output CFG to dot files",
          "type": "boolean",
          "default": false
        },
        "mincfg": {
          "title": "exp.mincfg",
          "description": "Try to minimize the number of CFG nodes.",
          "type": "boolean",
          "default": false
        },
        "earlyglobs": {
          "title": "exp.earlyglobs",
          "description":
            "Side-effecting of globals right after initialization.",
          "type": "boolean",
          "default": false
        },
        "region-offsets": {
          "title": "exp.region-offsets",
          "description": "Considers offsets for region accesses.",
          "type": "boolean",
          "default": false
        },
        "unique": {
          "title": "exp.unique",
          "description": "For types that have only one value.",
          "type": "array",
          "items": { "type": "string" },
          "default": []
        },
        "forward": {
          "title": "exp.forward",
          "description":
            "Use implicit forward propagation instead of the demand driven approach.",
          "type": "boolean",
          "default": false
        },
        "volatiles_are_top": {
          "title": "exp.volatiles_are_top",
          "description":
            "volatile and extern keywords set variables permanently to top",
          "type": "boolean",
          "default": true
        },
        "single-threaded": {
          "title": "exp.single-threaded",
          "description": "Ensures analyses that no threads are created.",
          "type": "boolean",
          "default": false
        },
        "globs_are_top": {
          "title": "exp.globs_are_top",
          "description": "Set globals permanently to top.",
          "type": "boolean",
          "default": false
        },
        "exclude_from_earlyglobs": {
          "title": "exp.exclude_from_earlyglobs",
          "description":
            "Global variables that should be handled flow-sensitively when using earlyglobs.",
          "type": "array",
          "items": { "type": "string" },
          "default": []
        },
        "exclude_from_invalidation" : {
          "title": "exp.exclude_from_invalidation",
          "description":
            "Global variables that should not be invalidated. This assures the analysis that such globals are only modified through known code",
          "type": "array",
          "items": { "type": "string" },
          "default": []
        },
        "g2html_path": {
          "title": "exp.g2html_path",
          "description": "Location of the g2html.jar file. If empty, then goblint executable directory is used.",
          "type": "string",
          "default": ""
        },
        "extraspecials": {
          "title": "exp.extraspecials",
          "description":
            "List of functions that must be analyzed as unknown extern functions",
          "type": "array",
          "items": { "type": "string" },
          "default": []
        },
        "no-narrow": {
          "title": "exp.no-narrow",
          "description": "Overwrite narrow a b = a",
          "type": "boolean",
          "default": false
        },
        "basic-blocks": {
          "title": "exp.basic-blocks",
          "description":
            "Only keep values for basic blocks instead of for every node. Should take longer but need less space.",
          "type": "boolean",
          "default": false
        },
        "fast_global_inits": {
          "title": "exp.fast_global_inits",
          "description":
            "Only generate one 'a[any_index] = x' for all assignments a[...] = x for a global array a[n].",
          "type": "boolean",
          "default": true
        },
        "architecture": {
          "title": "exp.architecture",
          "description": "Architecture for analysis, currently for witness",
          "type": "string",
          "enum": ["64bit", "32bit"],
          "default": "64bit"
        },
        "gcc_path": {
          "title": "exp.gcc_path",
          "description":
            "Location of gcc. Used to combine source files with cilly. Change to gcc-9 or another version on OS X (with gcc being clang by default cilly will fail otherwise).",
          "type": "string",
          "default": "/usr/bin/gcc"
        },
        "cpp-path": {
          "title": "exp.cpp-path",
          "description":
            "Path to C preprocessor (cpp) to use. If empty, then automatically searched.",
          "type": "string",
          "default": ""
        },
        "unrolling-factor": {
          "title": "exp.unrolling-factor",
          "description":
            "Sets the unrolling factor for the loopUnrollingVisitor.",
          "type": "integer",
          "default": 0
        },
        "hide-std-globals": {
          "title": "exp.hide-std-globals",
          "description": "Hide standard extern globals (e.g. `stdout`) from cluttering local states.",
          "type": "boolean",
          "default": true
        },
        "arg": {
          "title": "exp.arg",
          "description": "Abstract reachability graph (ARG) options",
          "type": "object",
          "properties": {
            "enabled": {
              "title": "exp.arg.enabled",
              "description": "Construct ARG.",
              "type": "boolean",
              "default": false
            },
            "id": {
              "title": "exp.arg.id",
              "description": "Which ARG node IDs to use? node/enumerate",
              "type": "string",
              "enum": ["node", "enumerate"],
              "default": "node"
            },
            "uncil": {
              "title": "exp.arg.uncil",
              "description":
                "Try to undo CIL control flow transformations in ARG",
              "type": "boolean",
              "default": false
            },
            "stack": {
              "title": "exp.arg.stack",
              "description": "Construct stacktrace-based ARG nodes",
              "type": "boolean",
              "default": false
            },
            "dot": {
              "title": "exp.arg.dot",
              "description": "ARG output as .dot file",
              "type": "object",
              "properties": {
                "path": {
                  "title": "exp.arg.dot.path",
                  "description": "ARG .dot file output path. Disabled if empty.",
                  "type": "string",
                  "default": ""
                },
                "node-label": {
                  "title": "exp.arg.dot.node-label",
                  "description": "Which ARG node labels to use? node/empty",
                  "type": "string",
                  "enum": ["node", "empty"],
                  "default": "node"
                }
              },
              "additionalProperties": false
            }
          },
          "additionalProperties": false
        }
      },
      "additionalProperties": false
    },
    "dbg": {
      "title": "Debugging",
      "description": "Debugging options",
      "type": "object",
      "properties": {
        "level": {
          "title": "dbg.level",
          "description": "Logging level.",
          "type": "string",
          "enum": ["debug", "info", "warning", "error", "result"],
          "default": "info"
        },
        "timing": {
          "title": "dbg.timing",
          "type": "object",
          "properties": {
            "enabled": {
              "title": "dbg.timing.enabled",
              "description": "Collect and output timing information.",
              "type": "boolean",
              "default": false
            },
            "tef": {
              "title": "dbg.timing.tef",
              "description": "Filename for Trace Event Format (TEF) output. Disabled if empty.",
              "type": "string",
              "default": ""
            }
          },
          "additionalProperties": false
        },
        "trace": {
          "title": "dbg.trace",
          "type": "object",
          "properties": {
            "context": {
              "title": "dbg.trace.context",
              "description": "Also print the context of solver variables.",
              "type": "boolean",
              "default": false
            }
          },
          "additionalProperties": false
        },
        "cilout": {
          "title": "dbg.cilout",
          "description": "Where to dump cil output",
          "type": "string",
          "default": ""
        },
        "justcil-printer": {
          "title": "dbg.justcil-printer",
          "description": "Printer to use for justcil: default, or clean (excludes line directives and builtin declarations).",
          "type": "string",
          "enum": ["default", "clean"],
          "default": "default"
        },
        "timeout": {
          "title": "dbg.timeout",
          "description":
            "Stop solver after this time. 0 means no timeout. Supports optional units h, m, s. E.g. 1m6s = 01m06s = 66; 6h = 6*60*60.",
          "type": "string",
          "default": "0"
        },
        "solver-stats-interval": {
          "title": "dbg.solver-stats-interval",
          "description":
            "Interval in seconds to print statistics while solving. Set to 0 to deactivate.",
          "type": "integer",
          "default": 10
        },
        "solver-signal": {
          "title": "dbg.solver-signal",
          "description":
            "Signal to print statistics while solving. Possible values: sigint (Ctrl+C), sigtstp (Ctrl+Z), sigquit (Ctrl+\\), sigusr1, sigusr2, sigalrm, sigprof etc. (see signal_of_string in gobSys.ml).",
          "type": "string",
          "default": "sigusr1"
        },
        "backtrace-signal": {
          "title": "dbg.backtrace-signal",
          "description":
            "Signal to print a raw backtrace on stderr. Possible values: sigint (Ctrl+C), sigtstp (Ctrl+Z), sigquit (Ctrl+\\), sigusr1, sigusr2, sigalrm, sigprof etc. (see signal_of_string in gobSys.ml).",
          "type": "string",
          "default": "sigusr2"
        },
        "solver-progress": {
          "title": "dbg.solver-progress",
          "description":
            "Used for debugging. Prints out a symbol on solving a rhs.",
          "type": "boolean",
          "default": false
        },
        "print_wpoints": {
          "title": "dbg.print_wpoints",
          "description":
            "Print the widening points after solving (does not include the removed wpoints during solving by the slr solvers). Currently only implemented in: slr*, td3.",
          "type": "boolean",
          "default": false
        },
        "slice": {
          "title": "dbg.slice",
          "type": "object",
          "properties": {
            "on": {
              "title": "dbg.slice.on",
              "description": "Turn slicer on or off.",
              "type": "boolean",
              "default": false
            },
            "n": {
              "title": "dbg.slice.n",
              "description": "How deep function stack do we analyze.",
              "type": "integer",
              "default": 10
            }
          },
          "additionalProperties": false
        },
        "warn_with_context": {
          "title": "dbg.warn_with_context",
          "description":
            "Keep warnings for different contexts apart (currently only done for asserts).",
          "type": "boolean",
          "default": false
        },
        "test": {
          "title": "dbg.test",
          "type": "object",
          "properties": {
            "domain": {
              "title": "dbg.test.domain",
              "description": "Test domain properties",
              "type": "boolean",
              "default": false
            }
          },
          "additionalProperties": false
        },
        "cilcfgdot": {
          "title": "dbg.cilcfgdot",
          "description": "Output dot files for CIL CFGs.",
          "type": "boolean",
          "default": false
        },
        "cfg": {
          "title": "dbg.cfg",
          "type": "object",
          "properties": {
            "loop-clusters": {
              "title": "dbg.cfg.loop-clusters",
              "description": "Add loop SCC clusters to CFG .dot output.",
              "type": "boolean",
              "default": false
            },
            "loop-unrolling": {
              "title": "dbg.cfg.loop-unrolling",
              "description": "Add dotted loop unrolling copy-of edges to CFG .dot output.",
              "type": "boolean",
              "default": false
            }
          },
          "additionalProperties": false
        },
        "compare_runs": {
          "title": "dbg.compare_runs",
          "type": "object",
          "properties": {
            "globsys": {
              "title": "dbg.compare_runs.globsys",
              "description": "Compare GlobConstrSys in compare_runs",
              "type": "boolean",
              "default": false
            },
            "eqsys": {
              "title": "dbg.compare_runs.eqsys",
              "description": "Compare EqConstrSys in compare_runs",
              "type": "boolean",
              "default": true
            },
            "global": {
              "title": "dbg.compare_runs.global",
              "description": "Compare globals in compare_runs",
              "type": "boolean",
              "default": false
            },
            "node": {
              "title": "dbg.compare_runs.node",
              "description": "Compare nodes (with joined contexts) in compare_runs",
              "type": "boolean",
              "default": false
            },
            "diff": {
              "title": "dbg.compare_runs.diff",
              "description": "Print differences",
              "type": "boolean",
              "default": false
            }
          },
          "additionalProperties": false
        },
        "print_tids": {
          "title": "dbg.print_tids",
          "description":
            "Should the analysis print information on the encountered TIDs",
          "type": "boolean",
          "default": false
        },
        "print_protection": {
          "title": "dbg.print_protection",
          "description":
            "Should the analysis print information on which globals are protected by which mutex?",
          "type": "boolean",
          "default": false
        },
        "run_cil_check" : {
          "title": "dbg.run_cil_check",
          "description":
            "Should the analysis call Check.checkFile after creating the CFG (helpful to verify that transformations respect CIL's invariants.",
          "type": "boolean",
          "default": false
        },
        "full-output": {
          "title": "dbg.full-output",
          "description": "Output abstract values, etc. with full internal details, without readability-oriented simplifications.",
          "type": "boolean",
          "default": false
        },
        "termination-bounds": {
          "title": "dbg.termination-bounds",
          "description": "Output loop iteration bounds for terminating loops when termination analysis is activated.",
          "type": "boolean",
          "default": false
        }
      },
      "additionalProperties": false
    },
    "warn": {
      "title": "Warnings",
      "description": "Filtering of warnings",
      "type": "object",
      "properties": {
        "assert": {
          "title": "warn.assert",
          "description": "Assert messages",
          "type": "boolean",
          "default": true
        },
        "behavior": {
          "title": "warn.behavior",
          "description": "undefined behavior warnings",
          "type": "boolean",
          "default": true
        },
        "call": {
          "title": "warn.call",
          "description": "function call warnings",
          "type": "boolean",
          "default": true
        },
        "integer": {
          "title": "warn.integer",
          "description": "integer (Overflow, Div_by_zero) warnings",
          "type": "boolean",
          "default": true
        },
        "float": {
          "title": "warn.float",
          "description": "float warnings",
          "type": "boolean",
          "default": true
        },
        "cast": {
          "title": "warn.cast",
          "description": "Cast (Type_mismatch(bug) warnings",
          "type": "boolean",
          "default": true
        },
        "race": {
          "title": "warn.race",
          "description": "Race warnings",
          "type": "boolean",
          "default": true
        },
        "deadlock": {
          "title": "warn.deadlock",
          "description": "Deadlock warnings",
          "type": "boolean",
          "default": true
        },
        "deadcode": {
          "title": "warn.deadcode",
          "description": "Dead code warnings",
          "type": "boolean",
          "default": true
        },
        "analyzer": {
          "title": "warn.analyzer",
          "description": "Analyzer messages",
          "type": "boolean",
          "default": true
        },
        "unsound": {
          "title": "warn.unsound",
          "description": "Unsoundness messages",
          "type": "boolean",
          "default": true
        },
        "imprecise": {
          "title": "warn.imprecise",
          "description": "Imprecision messages",
          "type": "boolean",
          "default": true
        },
        "witness": {
          "title": "warn.witness",
          "description": "Witness messages",
          "type": "boolean",
          "default": true
        },
        "program": {
          "title": "warn.program",
          "description": "Program messages",
          "type": "boolean",
          "default": true
        },
        "termination": {
          "title": "warn.termination",
          "description": "Non-Termination warning",
          "type": "boolean",
          "default": true
        },
        "unknown": {
          "title": "warn.unknown",
          "description": "Unknown (of string) warnings",
          "type": "boolean",
          "default": true
        },
        "error": {
          "title": "warn.error",
          "description": "Error severity messages",
          "type": "boolean",
          "default": true
        },
        "warning": {
          "title": "warn.warning",
          "description": "Warning severity messages",
          "type": "boolean",
          "default": true
        },
        "info": {
          "title": "warn.info",
          "description": "Info severity messages",
          "type": "boolean",
          "default": true
        },
        "debug": {
          "title": "warn.debug",
          "description": "Debug severity messages",
          "type": "boolean",
          "default": false
        },
        "success": {
          "title": "warn.success",
          "description": "Success severity messages",
          "type": "boolean",
          "default": true
        },
        "quote-code": {
          "title": "warn.quote-code",
          "description": "Quote code in message output.",
          "type": "boolean",
          "default": false
        },
        "race-threshold": {
          "title": "warn.race-threshold",
          "description": "Races with confidence at least threshold are warnings, lower are infos.",
          "type": "integer",
          "default": 0
        },
        "deterministic": {
          "title": "warn.deterministic",
          "description": "Output messages in deterministic order. Useful for cram testing.",
          "type": "boolean",
          "default": false
        },
        "memleak": {
          "title": "warn.memleak",
          "type":"object",
          "properties": {
            "memcleanup": {
              "title": "warn.memleak.memcleanup",
              "description": "Enable memory leak warnings only for violations of the SV-COMP \"valid-memcleanup\" category",
              "type": "boolean",
              "default": false
            },
            "memtrack": {
              "title": "warn.memleak.memtrack",
              "description": "Enable memory leak warnings only for violations of the SV-COMP \"valid-memtrack\" category",
              "type": "boolean",
              "default": false
            }
          },
          "additionalProperties": false
        }
      },
      "additionalProperties": false
    },
    "solvers": {
      "title": "solvers",
      "type": "object",
      "properties": {
        "td3": {
          "title": "solvers.td3",
          "type": "object",
          "properties": {
            "term": {
              "title": "solvers.td3.term",
              "description":
                "Should the td3 solver use the phased/terminating strategy?",
              "type": "boolean",
              "default": true
            },
            "side_widen": {
              "title": "solvers.td3.side_widen",
              "description":
                "When to widen in side. never: never widen, always: always widen, sides: widen if there are multiple side-effects from the same var resulting in a new value, cycle: widen if a called or a start var get destabilized, unstable_called: widen if any called var gets destabilized, unstable_self: widen if side-effected var gets destabilized, sides-pp: widen if there are multiple side-effects from the same program point resulting in a new value, sides-local: Widen with contributions from variables from which multiple side-effects leading to a new value originate.",
              "type": "string",
              "enum": ["never", "always", "sides", "cycle", "unstable_called", "unstable_self", "sides-pp","sides-local"],
              "default": "sides"
            },
            "side_widen_gas": {
              "title": "solvers.td3.side_widen_gas",
              "description":
                "Delay widening globals through side-effects. With a widening gas of N, the solver will perform widening only once unknown has grown through side-effects N times and the widening condition according to the side_widen policy has been met. A value of 0 behaves as before the feature was introduced.",
              "type": "integer",
              "default": 0
            },
            "widen_gas": {
              "title": "solvers.td3.widen_gas",
              "description":
                "Delay widening non-globals, i.e. unknowns with right hand sides. With a widening gas of N, the solver will perform widening only once unknown has grown N times. A value of 0 behaves as before the feature was introduced.",
              "type": "integer",
              "default": 0
            },
            "space": {
              "title": "solvers.td3.space",
              "description":
                "Should the td3 solver only keep values at widening points?",
              "type": "boolean",
              "default": false
            },
            "space_cache": {
              "title": "solvers.td3.space_cache",
              "description": "Should the td3-space solver cache values?",
              "type": "boolean",
              "default": true
            },
            "space_restore": {
              "title": "solvers.td3.space_restore",
              "description":
                "Should the td3-space solver restore values for non-widening-points? Not needed for generating warnings, but needed for inspecting output!",
              "type": "boolean",
              "default": true
            },
            "narrow-reuse": {
              "title": "solvers.td3.narrow-reuse",
              "description": "Reuse value when switching from widening to narrowing phase. Avoids one unnecessary re-evaluation.",
              "type": "boolean",
              "default": true
            },
            "narrow-globs": {
              "title": "solvers.td3.narrow-globs",
              "type": "object",
              "properties": {
                "enabled": {
                  "title": "solvers.td3.narrow-globs.enabled",
                  "description": "Individually track side-effects from different unknowns to enable narrowing of globals.",
                  "type": "boolean",
                  "default": false
                },
                "conservative-widen": {
                  "title": "solvers.td3.narrow-globs.conservative-widen",
                  "description": "Controls when to widen divided sides. true: Only widen on a side-effect, if joining would affect the overall value of the global. false: Always widen increasing/incomparable side-effects",
                  "type": "boolean",
                  "default": true
                },
                "immediate-growth": {
                  "title": "solvers.td3.narrow-globs.immediate-growth",
                  "description": "Controls when growing side-effects are applied. true: immediately when they are triggered. false: after the source unknown has been fully evaluated",
                  "type": "boolean",
                  "default": true
                },
                "narrow-gas": {
                  "title": "solvers.td3.narrow-globs.narrow-gas",
                  "description": "Limits the number of times a side-effect can switch from widening to narrowing to enforce termination. 0 disables narrowing, -1 allows narrowing infinitely often.",
                  "type": "integer",
                  "default": 5
                },
                "eliminate-dead": {
                  "title": "solvers.td3.narrow-globs.eliminate-dead",
                  "description": "side-effects that no longer occur are narrowed with bot.",
                  "type": "boolean",
                  "default": false
                }
              },
              "additionalProperties": false
            },
            "remove-wpoint": {
              "title": "solvers.td3.remove-wpoint",
              "description": "Remove widening points after narrowing phase. Enables a form of local restarting which increases precision of nested loops.",
              "type": "boolean",
              "default": true
            },
            "skip-unchanged-rhs" : {
              "title" : "solvers.td3.skip-unchanged-rhs",
              "description" : "Skip evaluation of RHS if all dependencies are unchanged - INCOMPATIBLE WITH RESTARTING",
              "type" : "boolean",
              "default": false
            },
            "restart": {
              "title": "solvers.td3.restart",
              "type": "object",
              "properties": {
                "wpoint": {
                  "title": "solvers.td3.restart.wpoint",
                  "type": "object",
                  "properties": {
                    "enabled": {
                      "title": "solvers.td3.restart.wpoint.enabled",
                      "description": "Restart wpoint to bot when (re-)detected. Allows incremental to avoid reusing and republishing imprecise local values due to globals (which get restarted).",
                      "type": "boolean",
                      "default": false
                    },
                    "once": {
                      "title": "solvers.td3.restart.wpoint.once",
                      "description": "Restart wpoint only on first detection. Useful for incremental loading.",
                      "type": "boolean",
                      "default": false
                    }
                  },
                  "additionalProperties": false
                }
              },
              "additionalProperties": false
            },
            "verify": {
              "title": "solvers.td3.verify",
              "description": "Check TD3 data structure invariants",
              "type": "boolean",
              "default": false
            },
            "parallel_domains" :{
              "title": "solvers.td3.parallel_domains",
              "description": "Maximal number of Domains that the solver can use in parallel. Only applies, when a solver of the 'td_parallel_*' family is used. If left at -1, the value of jobs will be used.",
              "type": "integer",
              "default": -1
            },
            "weak-deps": {
              "title": "solvers.td3.weak-deps",
              "description": "Handling of weak dependencies from demand: 'none' - as normal dependencies, 'eager' - solve immediately, 'lazy' - solve at top level.",
              "type": "string",
              "enum": ["none", "eager", "lazy"],
              "default": "none"
            }
          },
          "additionalProperties": false
        },
        "slr4": {
          "title": "solvers.slr4",
          "type": "object",
          "properties": {
            "restart_count": {
              "title": "solvers.slr4.restart_count",
              "description":
                "How many times SLR4 is allowed to switch from restarting iteration to increasing iteration.",
              "type": "integer",
              "default": 1
            }
          },
          "additionalProperties": false
        }
      },
      "additionalProperties": false
    },
    "witness": {
      "title": "witness",
      "type": "object",
      "properties": {
        "invariant": {
          "title": "witness.invariant",
          "type": "object",
          "properties": {
            "loop-head": {
              "title": "witness.invariant.loop-head",
              "description":
                "Emit invariants at loop heads",
              "type": "boolean",
              "default": true
            },
            "after-lock": {
              "title": "witness.invariant.after-lock",
              "description":
                "Emit invariants after mutex locking",
              "type": "boolean",
              "default": true
            },
            "other": {
              "title": "witness.invariant.other",
              "description":
                "Emit invariants at all other locations",
              "type": "boolean",
              "default": true
            },
            "split-conjunction": {
              "title": "witness.invariant.split-conjunction",
              "description": "Split conjunctive invariant to multiple invariants",
              "type": "boolean",
              "default": true
            },
            "accessed": {
              "title": "witness.invariant.accessed",
              "description": "Only emit invariants for locally accessed variables",
              "type": "boolean",
              "default": false
            },
            "full": {
              "title": "witness.invariant.full",
              "description":
                "Whether to dump assertions about all local variables or limitting it to modified ones where possible.",
              "type": "boolean",
              "default": true
            },
            "exact": {
              "title": "witness.invariant.exact",
              "description": "Emit exact invariants. They are useless for unassuming.",
              "type": "boolean",
              "default": true
            },
            "inexact-type-bounds": {
              "title": "witness.invariant.inexact-type-bounds",
              "description": "Emit inexact invariants matching type bounds.",
              "type": "boolean",
              "default": false
            },
            "exclude-vars": {
              "title": "witness.invariant.exclude-vars",
              "description": "OCaml Str regexes for variables to exclude from invariants.",
              "type": "array",
              "items": {
                "type": "string"
              },
              "default": [
                "tmp\\(___[0-9]+\\)?",
                "cond",
                "RETURN"
              ]
            },
            "all-locals": {
              "title": "witness.invariant.all-locals",
              "description": "Emit invariants for local variables under the assumption they are always in scope within their function.",
              "type": "boolean",
              "default": true
            },
            "goblint": {
              "title": "witness.invariant.goblint",
              "description": "Emit non-standard Goblint-specific invariants. Currently array invariants with all_index offsets.",
              "type": "boolean",
              "default": false
            },
            "typedefs": {
              "title": "witness.invariant.typedefs",
              "description": "Emit invariants with typedef-ed types (e.g. in casts). Our validator cannot parse these.",
              "type": "boolean",
              "default": true
            },
            "flow_insensitive-as": {
              "title": "witness.invariant.flow_insensitive-as",
              "description": "Emit flow-insensitive invariants as location invariants at certain locations.",
              "type": "string",
              "enum": ["invariant_set-flow_insensitive_invariant", "invariant_set-location_invariant"],
              "default": "invariant_set-flow_insensitive_invariant"
            }
          },
          "additionalProperties": false
        },
        "yaml": {
          "title": "witness.yaml",
          "type": "object",
          "properties": {
            "enabled": {
              "title": "witness.yaml.enabled",
              "description": "Output YAML witness",
              "type": "boolean",
              "default": false
            },
            "sv-comp-true-only": {
              "title": "witness.yaml.sv-comp-true-only",
              "description": "Only output YAML witness when SV-COMP result is \"true\".",
              "type": "boolean",
              "default": false
            },
            "format-version": {
              "title": "witness.yaml.format-version",
              "description": "YAML witness format version",
              "type": "string",
              "enum": [
                "2.0",
                "2.1",
                "2.1-goblint"
              ],
              "default": "2.1"
            },
            "entry-types": {
              "title": "witness.yaml.entry-types",
              "description": "YAML witness entry types to output/input.",
              "type": "array",
              "items": {
                "type": "string",
                "enum": [
                  "invariant_set",
                  "violation_sequence",
                  "ghost_instrumentation"
                ]
              },
              "default": [
                "invariant_set"
              ]
            },
            "invariant-types": {
              "title": "witness.yaml.invariant-types",
              "description": "YAML witness invariant types to output/input.",
              "type": "array",
              "items": {
                "type": "string",
                "enum": [
                  "location_invariant",
                  "loop_invariant",
                  "flow_insensitive_invariant"
                ]
              },
              "default": [
                "location_invariant",
                "loop_invariant"
              ]
            },
            "path": {
              "title": "witness.yaml.path",
              "description": "YAML witness output path",
              "type": "string",
              "default": "witness.yml"
            },
            "validate": {
              "title": "witness.yaml.validate",
              "description": "YAML witness input path",
              "type": "string",
              "default": ""
            },
            "strict": {
              "title": "witness.yaml.strict",
              "description": "Fail YAML witness validation if there's an error/unsupported/disabled entry.",
              "type": "boolean",
              "default": false
            },
            "unassume": {
              "title": "witness.yaml.unassume",
              "description": "YAML witness input path",
              "type": "string",
              "default": ""
            }
          },
          "additionalProperties": false
        }
      },
      "additionalProperties": false
    }
  },
  "additionalProperties": false
}
