# The implementation of the contracts is done in two visits.
#
# - First step, the visitor analyzes and constructs the contracts
- # for each class (invariant) and method (expects, ensures).
+ # for each class (invariant) and method (expect, ensure).
#
# - Second step the visitor analyzes each `ASendExpr` to see
# if the callsite calls a method with a contract. If this is
assert contract_propdef != null
return contract_propdef
end
+
+ # Verification if the construction of the contract is necessary.
+ # Three cases are checked for `expect`:
+ #
+ # - Is the `--full-contract` option it's use?
+ # - Is the method is in the main package
+ # - Is the method is in a direct imported package.
+ #
+ fun check_usage_expect(actual_mmodule: MModule): Bool
+ do
+ var main_package = mainmodule.mpackage
+ var actual_package = actual_mmodule.mpackage
+ if main_package != null and actual_package != null then
+ var condition_direct_arc = toolcontext.modelbuilder.model.mpackage_importation_graph.has_arc(main_package, actual_package)
+ return toolcontext.opt_full_contract.value or condition_direct_arc or main_package == actual_package
+ end
+ return false
+ end
+
+ # Verification if the construction of the contract is necessary.
+ # Two cases are checked for `ensure`:
+ #
+ # - Is the `--full-contract` option it's use?
+ # - Is the method is in the main package
+ #
+ fun check_usage_ensure(actual_mmodule: MModule): Bool
+ do
+ return toolcontext.opt_full_contract.value or mainmodule.mpackage == actual_mmodule.mpackage
+ end
+
end
# This visitor checks the `callsite` to see if the target `mpropdef` has a contract.
# If it's the case the callsite is replaced by another callsite to the contract method.
private fun drive_method_contract(callsite: CallSite): CallSite
do
- if callsite.mpropdef.has_contract then
+ if callsite.mproperty.mcontract_facet != null then
var contract_facet = callsite.mproperty.mcontract_facet
var visited_mpropdef = visited_method.mpropdef
assert contract_facet != null and visited_mpropdef != null
- var unsafe_mtype = callsite.recv.resolve_for(callsite.recv, callsite.anchor, visited_mpropdef.mclassdef.mmodule, false)
-
- # This check is needed because the contract can appear after the introduction.
- if unsafe_mtype.has_mproperty(visited_method.mpropdef.mclassdef.mmodule, contract_facet) then
- var type_visitor = new TypeVisitor(toolcontext.modelbuilder, visited_mpropdef)
- var drived_callsite = type_visitor.build_callsite_by_property(visited_method, callsite.recv, contract_facet, callsite.recv_is_self)
- # This never happen this check is here for debug
- assert drived_callsite != null
- return drived_callsite
- end
+ var type_visitor = new TypeVisitor(toolcontext.modelbuilder, visited_mpropdef)
+ var drived_callsite = type_visitor.build_callsite_by_property(visited_method, callsite.recv, contract_facet, callsite.recv_is_self)
+ # This never happen this check is here for debug
+ assert drived_callsite != null
+ return drived_callsite
end
return callsite
end
# Returns the conditions of annotation parameters in the form of and expr
# exemple:
- # the contract ensures(true, i == 10, f >= 1.0)
+ # the contract ensure(true, i == 10, f >= 1.0)
# return this condition (true and i == 10 and f >= 1.0)
private fun construct_condition(v : ContractsVisitor): AExpr
do
# Define the name of the contract
fun contract_name: String is abstract
- # Checking if the use of the contract is necessary
- private fun check_usage(v: ContractsVisitor, actual_mmodule: MModule): Bool is abstract
-
# Method use to diplay warning when the contract is not present at the introduction
private fun no_intro_contract(v: ContractsVisitor, a: AAnnotation)do end
super MContract
# Define the name of the contract
- redef fun contract_name: String do return "expects"
-
- # Verification if the construction of the contract is necessary.
- # Three cases are checked for `expects`:
- #
- # - Is the `--full-contract` option it's use?
- # - Is the method is in the main package
- # - Is the method is in a direct imported package.
- #
- redef fun check_usage(v: ContractsVisitor, actual_mmodule: MModule): Bool
- do
- var main_package = v.mainmodule.mpackage
- var actual_package = actual_mmodule.mpackage
- if main_package != null and actual_package != null then
- var condition_direct_arc = v.toolcontext.modelbuilder.model.mpackage_importation_graph.has_arc(main_package, actual_package)
- return v.toolcontext.opt_full_contract.value or condition_direct_arc or main_package == actual_package
- end
- return false
- end
+ redef fun contract_name: String do return "expect"
# Display warning if no contract is defined at introduction `expect`,
# because if no contract is defined at the introduction the added
# ~~~nitish
# class A
# fun bar [...]
- # fun _bar_expects([...])
+ # fun _bar_expect([...])
# do
# [empty contract]
# end
# end
#
# redef class A
- # redef fun bar is expects(contract_condition)
- # redef fun _bar_expects([...])
+ # redef fun bar is expect(contract_condition)
+ # redef fun _bar_expect([...])
# do
# if not (contract_condition) then super
# end
end
end
-# The root of all contracts where the call is after the execution of the original method (`invariants` and `ensures`).
+# The root of all contracts where the call is after the execution of the original method (`invariant` and `ensure`).
abstract class BottomMContract
super MContract
- # Verification if the construction of the contract is necessary.
- # Two cases are checked for `expects`:
- #
- # - Is the `--full-contract` option it's use?
- # - Is the method is in the main package
- #
- redef fun check_usage(v: ContractsVisitor, actual_mmodule: MModule): Bool
- do
- return v.toolcontext.opt_full_contract.value or v.mainmodule.mpackage == actual_mmodule.mpackage
- end
-
redef fun create_nblock(v: ContractsVisitor, n_condition: AExpr, args: Array[AExpr]): ABlockExpr
do
var tid = new TId.init_tk(v.current_location)
super BottomMContract
# Define the name of the contract
- redef fun contract_name: String do return "ensures"
+ redef fun contract_name: String do return "ensure"
redef fun adapt_specific_msignature(m_signature: MSignature): MSignature
do
do
if self.mensure != null then return true
# build a new `MEnsure` contract
- self.mensure = new MEnsure(intro_mclassdef, "_ensures_{name}", intro_mclassdef.location, public_visibility)
+ self.mensure = new MEnsure(intro_mclassdef, "_ensure_{name}", intro_mclassdef.location, public_visibility)
return false
end
do
if self.mexpect != null then return true
# build a new `MExpect` contract
- self.mexpect = new MExpect(intro_mclassdef, "_expects_{name}", intro_mclassdef.location, public_visibility)
+ self.mexpect = new MExpect(intro_mclassdef, "_expect_{name}", intro_mclassdef.location, public_visibility)
return false
end
do
if self.mcontract_facet != null then return true
# build a new `MMethod` contract
- self.mcontract_facet = new MMethod(mpropdef.mclassdef, "_contract_{name}", mpropdef.mclassdef.location, public_visibility)
+ self.mcontract_facet = new MMethod(intro_mclassdef, "_contract_{name}", intro_mclassdef.location, public_visibility)
return false
end
end
# Verification of the contract facet
# Check if a contract facet already exists to use it again or if it is necessary to create it.
- private fun check_contract_facet(v: ContractsVisitor, n_signature: ASignature, mcontract: MContract, exist_contract: Bool)
+ private fun check_contract_facet(v: ContractsVisitor, n_signature: ASignature, classdef: MClassDef, mcontract: MContract, exist_contract: Bool)
do
var exist_contract_facet = mproperty.check_exist_contract_facet(self)
if exist_contract_facet and exist_contract then return
var contract_facet: AMethPropdef
if not exist_contract_facet then
+ # If has no contract facet in intro just create it
+ if classdef != mproperty.intro_mclassdef then create_contract_facet(v, mproperty.intro_mclassdef, n_signature)
# If has no contract facet just create it
- contract_facet = create_contract_facet(v, n_signature)
+ contract_facet = create_contract_facet(v, classdef, n_signature)
else
- # Check if the contract facet already exist in this context (in this mclassdef)
- if mclassdef.mpropdefs_by_property.has_key(mproperty.mcontract_facet) then
+ # Check if the contract facet already exist in this context (in this classdef)
+ if classdef.mpropdefs_by_property.has_key(mproperty.mcontract_facet) then
# get the define
- contract_facet = v.toolcontext.modelbuilder.mpropdef2node(mclassdef.mpropdefs_by_property[mproperty.mcontract_facet]).as(AMethPropdef)
+ contract_facet = v.toolcontext.modelbuilder.mpropdef2node(classdef.mpropdefs_by_property[mproperty.mcontract_facet]).as(AMethPropdef)
else
# create a new contract facet definition
- contract_facet = create_contract_facet(v, n_signature)
+ contract_facet = create_contract_facet(v, classdef, n_signature)
var block = v.ast_builder.make_block
# super call to the contract facet
var n_super_call = v.ast_builder.make_super_call(n_signature.make_parameter_read(v.ast_builder), null)
end
# Method to create a contract facet of the method
- private fun create_contract_facet(v: ContractsVisitor, n_signature: ASignature): AMethPropdef
+ private fun create_contract_facet(v: ContractsVisitor, classdef: MClassDef, n_signature: ASignature): AMethPropdef
do
var contract_facet = mproperty.mcontract_facet
assert contract_facet != null
var m_signature: nullable MSignature = null
if mproperty.intro.msignature != null then m_signature = mproperty.intro.msignature.clone
- var n_contractdef = mclassdef.mclass.create_empty_method(v, contract_facet, mclassdef, m_signature, n_signature)
+ var n_contractdef = classdef.mclass.create_empty_method(v, contract_facet, classdef, m_signature, n_signature)
# FIXME set the location because the callsite creation need the node location
n_contractdef.location = v.current_location
n_contractdef.validate
private fun construct_contract(v: ContractsVisitor, n_signature: ASignature, n_annotation: AAnnotation, mcontract: MContract, exist_contract: Bool)
do
if check_same_contract(v, n_annotation, mcontract) then return
- # Check if the contract is necessary
- if not mcontract.check_usage(v, mclassdef.mmodule) then return
if not exist_contract and not is_intro then no_intro_contract(v, n_signature, mcontract, n_annotation)
v.define_signature(mcontract, n_signature, mproperty.intro.msignature)
var conditiondef = v.build_contract(n_annotation, mcontract, mclassdef)
- check_contract_facet(v, n_signature.clone, mcontract, exist_contract)
+ check_contract_facet(v, n_signature.clone, mclassdef, mcontract, exist_contract)
has_contract = true
end
# Is the contract already defined in the context
#
# Exemple :
- # fun foo is expects([...]), expects([...])
+ # fun foo is expect([...]), expect([...])
#
- # Here `check_same_contract` display an error when the second expects is processed
+ # Here `check_same_contract` display an error when the second expect is processed
private fun check_same_contract(v: ContractsVisitor, n_annotation: AAnnotation ,mcontract: MContract): Bool
do
if self.mclassdef.mpropdefs_by_property.has_key(mcontract) then
redef class AMethPropdef
- # Execute all method verification scope flow and typing.
- # It also execute an ast validation to define all parents and all locations
- private fun do_all(toolcontext: ToolContext)
- do
- self.validate
- # FIXME: The `do_` usage it is maybe to much (verification...). Solution: Cut the `do_` methods into simpler parts
- self.do_scope(toolcontext)
- self.do_flow(toolcontext)
- self.do_typing(toolcontext.modelbuilder)
- end
-
# Entry point to create a contract (verification of inheritance, or new contract).
redef fun create_contracts(v)
do
# If this is the case, we built the appropriate contract.
private fun check_annotation(v: ContractsVisitor, n_annotation: AAnnotation)
do
- if n_annotation.name == "expects" then
+ if n_annotation.name == "expect" then
+ if not v.check_usage_expect(mpropdef.mclassdef.mmodule) then return
var exist_contract = mpropdef.mproperty.check_exist_expect
mpropdef.construct_contract(v, self.n_signature.as(not null), n_annotation, mpropdef.mproperty.mexpect.as(not null), exist_contract)
- else if n_annotation.name == "ensures" then
+ else if n_annotation.name == "ensure" then
+ if not v.check_usage_ensure(mpropdef.mclassdef.mmodule) then return
var exist_contract = mpropdef.mproperty.check_exist_ensure
mpropdef.construct_contract(v, self.n_signature.as(not null), n_annotation, mpropdef.mproperty.mensure.as(not null), exist_contract)
else if n_annotation.name == "no_contract" then