+
+ var bool_false = new AFalseExpr.make(mainmodule.bool_type)
+ var n_in_contract_attribute = toolcontext.modelbuilder.create_attribute_from_name("__in_contract_", sys_class.intro, mainmodule.bool_type, public_visibility).create_setter(toolcontext.modelbuilder, true).define_default(bool_false)
+
+ in_contract_attribute = n_in_contract_attribute.mpropdef.mproperty
+ end
+
+ # Return the `_in_contract_` attribute.
+ # If the attribute `_in_contract_` does not exist it's injected with `inject_incontract_in_sys`
+ private fun get_incontract: MAttribute
+ do
+ if self.in_contract_attribute == null then inject_incontract_in_sys
+ return in_contract_attribute.as(not null)
+ end
+
+ # Return an `AIfExpr` with the contract encapsulated by an `if` to check if it's already in a contract verification.
+ #
+ # Example:
+ # ~~~nitish
+ # class A
+ # fun bar([...]) is except([...])
+ #
+ # fun _contract_bar([...])
+ # do
+ # if not sys._in_contract_ then
+ # sys._in_contract_ = true
+ # _bar_expect([...])
+ # sys._in_contract_ = false
+ # end
+ # bar([...])
+ # end
+ #
+ # fun _bar_expect([...])
+ # end
+ # ~~~~
+ #
+ private fun encapsulated_contract_call(visited_method: AMethPropdef, call_to_contracts: Array[ACallExpr]): AIfExpr
+ do
+ var sys_property = toolcontext.modelbuilder.model.get_mproperties_by_name("sys").first.as(MMethod)
+ var callsite_sys = ast_builder.create_callsite(toolcontext.modelbuilder, visited_method, sys_property, true)
+
+ var incontract_attribute = get_incontract
+
+ var callsite_get_incontract = ast_builder.create_callsite(toolcontext.modelbuilder, visited_method, incontract_attribute.getter.as(MMethod), false)
+ var callsite_set_incontract = ast_builder.create_callsite(toolcontext.modelbuilder, visited_method, incontract_attribute.setter.as(MMethod), false)
+
+ var n_condition = ast_builder.make_not(ast_builder.make_call(ast_builder.make_call(new ASelfExpr, callsite_sys, null), callsite_get_incontract, null))
+
+ var n_if = ast_builder.make_if(n_condition, null)
+
+ var if_then_block = n_if.n_then.as(ABlockExpr)
+
+ if_then_block.add(ast_builder.make_call(ast_builder.make_call(new ASelfExpr, callsite_sys, null), callsite_set_incontract, [new ATrueExpr.make(mainmodule.bool_type)]))
+ if_then_block.add_all(call_to_contracts)
+ if_then_block.add(ast_builder.make_call(ast_builder.make_call(new ASelfExpr, callsite_sys, null), callsite_set_incontract, [new AFalseExpr.make(mainmodule.bool_type)]))
+
+ return n_if