diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml index 96ce12b2d8..a8d8e5d087 100644 --- a/src/transform/evalAssert.ml +++ b/src/transform/evalAssert.ml @@ -27,7 +27,7 @@ module EvalAssert = struct let surroundByAtomic = true (* variable for generating __goblint_check(exp) instead of __VERIFIER_assert(exp) *) - let goblintCheck () = GobConfig.get_bool "trans.goblint-check" + let goblintCheck () = GobConfig.get_bool "trans.assert.goblint-check" (* Cannot use Cilfacade.name_fundecs as assert() is external and has no fundec *) let ass () = if goblintCheck () then makeVarinfo true "__goblint_check" (TVoid []) else makeVarinfo true "__VERIFIER_assert" (TVoid []) diff --git a/src/util/options.schema.json b/src/util/options.schema.json index 2f79a1e509..c2b895d608 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -1493,11 +1493,19 @@ "type":"string", "default": "transformed.c" }, - "goblint-check" : { - "title": "trans.goblint-check", - "description": "Write __goblint_check(exp) in the file instead of __VERIFIER_assert(exp).", - "type": "boolean", - "default": false + "assert" : { + "title": "trans.assert", + "type": "object", + "properties": { + "goblint-check": { + "title": "trans.assert.goblint-check", + "description": + "Write __goblint_check(exp) in the file instead of __VERIFIER_assert(exp).", + "type": "boolean", + "default": false + } + }, + "additionalProperties": false } }, "additionalProperties": false