# FIXME Split the module in three parts: extension of the modele, building phase and the "re-driving"
module contracts
-import astbuilder
import parse_annotations
import phase
import semantize
+intrude import model_contract
+intrude import astbuilder
intrude import modelize_property
intrude import scope
intrude import typing
# if the callsite calls a method with a contract. If this is
# the case the callsite is replaced by another callsite to the contract method.
fun do_contracts(toolcontext: ToolContext) do
+ var ast_builder = new ASTBuilder(mmodule.as(not null))
#
- var contract_visitor = new ContractsVisitor(toolcontext, toolcontext.modelbuilder.identified_modules.first, self, new ASTBuilder(mmodule.as(not null)))
+ var contract_visitor = new ContractsVisitor(toolcontext, toolcontext.modelbuilder.identified_modules.first, self, ast_builder)
contract_visitor.enter_visit(self)
#
- var callsite_visitor = new CallSiteVisitor(toolcontext)
+ var callsite_visitor = new CallSiteVisitor(toolcontext, ast_builder)
callsite_visitor.enter_visit(self)
end
end
-# This visitor checks the `AMethPropdef` and the `AClassDef` to check if they have a contract annotation or it's a redefinition with a inheritance contract
+# Visitor to build all contracts.
private class ContractsVisitor
super Visitor
+ # Instance of the toolcontext
var toolcontext: ToolContext
# The main module
var current_location: Location is noinit
# Is the contrat is an introduction or not?
+ # This attribute has the same value as the `is_intro` of the propdef attached to the contract.
+ # Note : For MClassDef `is_intro_contract == false`. This is due to the fact that a method for checking invariants is systematically added to the root object class.
var is_intro_contract: Bool is noinit
# Actual visited class
# is `no_contract` annotation was found
var find_no_contract = false
+ # The reference to the `in_contract` attribute.
+ # This attribute is used to disable contract verification when you are already in a contract verification.
+ # Keep the `in_contract` attribute to avoid searching at each contrat
+ var in_contract_attribute: nullable MAttribute = null
+
redef fun visit(node)
do
node.create_contracts(self)
end
# Define the new contract take in consideration that an old contract exist or not
- private fun build_contract(n_annotation: AAnnotation, mcontract: MContract, mclassdef: MClassDef): MMethodDef
+ private fun build_contract(n_annotations: Array[AAnnotation], mcontract: MContract, mclassdef: MClassDef)
do
- self.current_location = n_annotation.location
+ var n_conditions = new Array[AExpr]
# Retrieving the expression provided in the annotation
- var n_condition = n_annotation.construct_condition(self)
- var m_contractdef: AMethPropdef
+ for n_annotation in n_annotations do n_conditions.add n_annotation.construct_condition(self)
if is_intro_contract then
# Create new contract method
- m_contractdef = mcontract.create_intro_contract(self, n_condition, mclassdef)
+ mcontract.create_intro_contract(self, n_conditions, mclassdef)
else
# Create a redef of contract to take in consideration the new condition
- m_contractdef = mcontract.create_subcontract(self, n_condition, mclassdef)
+ mcontract.create_subcontract(self, n_conditions, mclassdef)
end
- var contract_propdef = m_contractdef.mpropdef
- # The contract has a null mpropdef, this should never happen
- 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.
+ # - Was the `--full-contract` option passed?
+ # - 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
# 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
+ # - Was the `--full-contract` option passed?
+ # - 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
+ # Inject the incontract attribute (`_in_contract_`) in the `Sys` class
+ # This attribute allows to check if the contract need to be executed
+ private fun inject_incontract_in_sys
+ do
+ # If the `in_contract_attribute` already know just return
+ if in_contract_attribute != null then return
+
+ var sys_class = toolcontext.modelbuilder.get_mclass_by_name(visited_module, mainmodule, "Sys")
+
+ # Try to get the `in_contract` property, if it has already defined in a previously visited module.
+ var in_contract_property = toolcontext.modelbuilder.try_get_mproperty_by_name(visited_module, sys_class.intro, "__in_contract_")
+ if in_contract_property != null then
+ self.in_contract_attribute = in_contract_property.as(MAttribute)
+ return
+ end
+
+ 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
+ end
end
# This visitor checks the `callsite` to see if the target `mpropdef` has a contract.
private class CallSiteVisitor
super Visitor
+ # Instance of the toolcontext
var toolcontext: ToolContext
+ var ast_builder: ASTBuilder
+
# Actual visited method
- var visited_method: APropdef is noinit
+ var visited_propdef: APropdef is noinit
redef fun visit(node)
do
# 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.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 contract_facet = callsite.mproperty.mcontract_facet
+ var visited_mpropdef = visited_propdef.mpropdef
- 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
+ if visited_mpropdef isa MContract or visited_mpropdef isa MFacet then return callsite
+ if visited_mpropdef == null or contract_facet == null then return callsite
+
+ return ast_builder.create_callsite(toolcontext.modelbuilder, visited_propdef, contract_facet, callsite.recv_is_self)
end
end
redef class AAnnotation
- # Returns the conditions of annotation parameters in the form of and expr
- # exemple:
- # the contract ensure(true, i == 10, f >= 1.0)
- # return this condition (true and i == 10 and f >= 1.0)
+ # Returns the conditions of annotation parameters. If there are several parameters, the result is an `AAndExpr`
+ # Example:
+ # 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
var n_condition = n_args.first
end
end
-# The root of all contracts
-#
-# The objective of this class is to provide the set
-# of services must be implemented or provided by a contract
-abstract class MContract
- super MMethod
-
- # Define the name of the contract
- fun contract_name: String is abstract
+redef class MContract
# 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
+ private fun no_intro_contract(v: ContractsVisitor, a: Array[AAnnotation])do end
# Creating specific inheritance block contract
- private fun create_nblock(v: ContractsVisitor, n_condition: AExpr, args: Array[AExpr]): ABlockExpr is abstract
+ #
+ # `super_args` : Correspond to the `super` call arguments
+ private fun create_inherit_nblock(v: ContractsVisitor, n_conditions: Array[AExpr], super_args: Array[AExpr]): ABlockExpr is abstract
# Method to adapt the `n_mpropdef.n_block` to the contract
private fun adapt_block_to_contract(v: ContractsVisitor, n_mpropdef: AMethPropdef) is abstract
# Adapt the msignature specifically for the contract method
- private fun adapt_specific_msignature(m_signature: MSignature): MSignature do return m_signature.adapt_to_condition
+ private fun adapt_specific_msignature(m_signature: MSignature): MSignature do return m_signature.adapt_to_contract
# Adapt the nsignature specifically for the contract method
- private fun adapt_specific_nsignature(n_signature: ASignature): ASignature do return n_signature.adapt_to_condition(null)
+ private fun adapt_specific_nsignature(n_signature: ASignature): ASignature do return n_signature.adapt_to_contract
# Adapt the `m_signature` to the contract
# If it is not null call the specific adapt `m_signature` for the contract
# Create the initial contract (intro)
# All contracts have the same implementation for the introduction.
#
+ # Example:
+ # ~~~nitish
# fun contrat([...])
# do
# assert contract_condition
# end
+ # ~~~
#
- private fun create_intro_contract(v: ContractsVisitor, n_condition: nullable AExpr, mclassdef: MClassDef): AMethPropdef
+ private fun create_intro_contract(v: ContractsVisitor, n_conditions: Array[AExpr], mclassdef: MClassDef)
do
var n_block = v.ast_builder.make_block
- if n_condition != null then
+ for n_condition in n_conditions do
# Create a new tid to set the name of the assert for more explicit error
- var tid = new TId.init_tk(self.location)
- tid.text = "{self.contract_name}"
- n_block.add v.ast_builder.make_assert(tid, n_condition, null)
+ var tid = new TId.init_tk(n_condition.location)
+ tid.text = "{n_condition.location.text}"
+ var n_assert = v.ast_builder.make_assert(tid, n_condition, null)
+ # Define the assert location to reference the annoation
+ n_assert.location = n_condition.location
+ n_block.add n_assert
end
- return make_contract(v, n_block, mclassdef)
+ make_contract(v, n_block, mclassdef)
end
- # Create a contract with old (super) and the new conditions
- private fun create_subcontract(v: ContractsVisitor, ncondition: nullable AExpr, mclassdef: MClassDef): AMethPropdef
+ # Create a contract to check the old (super call) and the new conditions
+ #
+ # Example:
+ # ~~~nitish
+ # fun contrat([...])
+ # do
+ # super # Call the old contracts
+ # assert new_condition
+ # end
+ # ~~~
+ #
+ private fun create_subcontract(v: ContractsVisitor, n_conditions: Array[AExpr], mclassdef: MClassDef)
do
var args = v.n_signature.make_parameter_read(v.ast_builder)
var n_block = v.ast_builder.make_block
- if ncondition != null then n_block = self.create_nblock(v, ncondition, args)
- return make_contract(v, n_block, mclassdef)
+ n_block = self.create_inherit_nblock(v, n_conditions, args)
+ make_contract(v, n_block, mclassdef)
end
# Build a method with a specific block `n_block` in a specified `mclassdef`
- private fun make_contract(v: ContractsVisitor, n_block: AExpr, mclassdef: MClassDef): AMethPropdef
+ private fun make_contract(v: ContractsVisitor, n_block: AExpr, mclassdef: MClassDef)
do
var n_contractdef = intro_mclassdef.mclass.create_empty_method(v, self, mclassdef, v.m_signature, v.n_signature)
n_contractdef.n_block = n_block
# Define the location of the new method for corresponding of the annotation location
n_contractdef.location = v.current_location
n_contractdef.do_all(v.toolcontext)
- return n_contractdef
end
end
-# A expect (precondition) contract representation
-# This method check if the requirements of the called method is true.
-class MExpect
- super MContract
-
- # Define the name of the contract
- redef fun contract_name: String do return "expect"
+redef class MExpect
# Display warning if no contract is defined at introduction `expect`,
# because if no contract is defined at the introduction the added
# contracts will not cause any error even if they are not satisfied.
#
- # exemple
+ # Example:
# ~~~nitish
# class A
# fun bar [...]
# redef fun bar is expect(contract_condition)
# redef fun _bar_expect([...])
# do
- # if not (contract_condition) then super
+ # if (contract_condition) then return
+ # super
# end
# end
# ~~~~
#
- redef fun no_intro_contract(v: ContractsVisitor, a: AAnnotation)
+ redef fun no_intro_contract(v: ContractsVisitor, a: Array[AAnnotation])
do
- v.toolcontext.warning(a.location,"","Useless contract: No contract defined at the introduction of the method")
+ v.toolcontext.warning(a.first.location,"useless_contract","Useless contract: No contract defined at the introduction of the method")
end
- redef fun create_nblock(v: ContractsVisitor, n_condition: AExpr, args: Array[AExpr]): ABlockExpr
+ redef fun create_inherit_nblock(v: ContractsVisitor, n_conditions: Array[AExpr], super_args: Array[AExpr]): ABlockExpr
do
- # Creating the if expression with the new condition
- var if_block = v.ast_builder.make_if(n_condition, n_condition.mtype)
- # Creating and adding return expr to the then case
- if_block.n_then = v.ast_builder.make_return(null)
- # Creating the super call to the contract and adding this to else case
- if_block.n_else = v.ast_builder.make_super_call(args,null)
var n_block = v.ast_builder.make_block
- n_block.add if_block
+ for n_condition in n_conditions do
+ # Creating the if expression with the new condition
+ var if_block = v.ast_builder.make_if(n_condition, n_condition.mtype)
+ # Creating and adding return expr to the then case
+ if_block.n_then = v.ast_builder.make_return
+ if_block.location = n_condition.location
+ n_block.add if_block
+ end
+ n_block.add v.ast_builder.make_super_call(super_args)
return n_block
end
end
end
-# The root of all contracts where the call is after the execution of the original method (`invariant` and `ensure`).
-abstract class BottomMContract
- super MContract
+redef class BottomMContract
- redef fun create_nblock(v: ContractsVisitor, n_condition: AExpr, args: Array[AExpr]): ABlockExpr
+ redef fun create_inherit_nblock(v: ContractsVisitor, n_conditions: Array[AExpr], super_args: Array[AExpr]): ABlockExpr
do
- var tid = new TId.init_tk(v.current_location)
- tid.text = "{contract_name}"
- # Creating the assert expression with the new condition
- var assert_block = v.ast_builder.make_assert(tid,n_condition,null)
- # Creating the super call to the contract
- var super_call = v.ast_builder.make_super_call(args,null)
# Define contract block
var n_block = v.ast_builder.make_block
- # Adding the expressions to the block
+
+ var super_call = v.ast_builder.make_super_call(super_args)
+
n_block.add super_call
- n_block.add assert_block
+ for n_condition in n_conditions do
+ var tid = new TId.init_tk(n_condition.location)
+ tid.text = "{n_condition.location.text}"
+ # Creating the assert expression with the new condition
+ var n_assert = v.ast_builder.make_assert(tid, n_condition)
+ n_assert.location = n_condition.location
+ n_block.add n_assert
+ end
return n_block
end
- # Inject the result variable in the `n_block` of the given `n_mpropdef`.
+ # Inject the `result` variable into the `n_block` of the given n_mpropdef`.
+ #
+ # The purpose of the variable is to capture return values to use it in contracts.
private fun inject_result(v: ContractsVisitor, n_mpropdef: AMethPropdef, ret_type: MType): Variable
do
var actual_block = n_mpropdef.n_block
end
end
-# A ensure (postcondition) representation
-# This method check if the called method respects the expectations of the caller.
-class MEnsure
- super BottomMContract
-
- # Define the name of the contract
- redef fun contract_name: String do return "ensure"
+redef class MEnsure
redef fun adapt_specific_msignature(m_signature: MSignature): MSignature
do
end
end
-redef class MMethod
-
- # The contract facet of the method
- # it's representing the method with contract
- # This method call the contract and the method
- var mcontract_facet: nullable MMethod = null
-
- # The expected contract method
- var mexpect: nullable MExpect = null
-
- # The ensure contract method
- var mensure: nullable MEnsure = null
-
- # Check if the MMethod has no ensure contract
- # if this is the case returns false and built it
- # else return true
- private fun check_exist_ensure: Bool
- do
- if self.mensure != null then return true
- # build a new `MEnsure` contract
- self.mensure = new MEnsure(intro_mclassdef, "_ensure_{name}", intro_mclassdef.location, public_visibility)
- return false
- end
-
- # Check if the MMethod has no expect contract
- # if this is the case returns false and built it
- # else return true
- private fun check_exist_expect: Bool
- do
- if self.mexpect != null then return true
- # build a new `MExpect` contract
- self.mexpect = new MExpect(intro_mclassdef, "_expect_{name}", intro_mclassdef.location, public_visibility)
- return false
- end
-
- # Check if the MMethod has an contract facet
- # If the method has no contract facet she create it
- private fun check_exist_contract_facet(mpropdef : MMethodDef): Bool
- do
- if self.mcontract_facet != null then return true
- # build a new `MMethod` contract
- self.mcontract_facet = new MMethod(intro_mclassdef, "_contract_{name}", intro_mclassdef.location, public_visibility)
- return false
- end
-end
-
redef class MMethodDef
# 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, classdef: MClassDef, mcontract: MContract, exist_contract: Bool)
do
- var exist_contract_facet = mproperty.check_exist_contract_facet(self)
+ var exist_contract_facet = mproperty.has_contract_facet
if exist_contract_facet and exist_contract then return
var contract_facet: AMethPropdef
# Method to create a contract facet of the method
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 contract_facet = mproperty.build_contract_facet
# Defines the contract phase is an init or not
# it is necessary to use the contracts on constructor
contract_facet.is_init = self.mproperty.is_init
end
# Entry point to build contract (define the contract facet and define the contract method verification)
- private fun construct_contract(v: ContractsVisitor, n_signature: ASignature, n_annotation: AAnnotation, mcontract: MContract, exist_contract: Bool)
+ private fun construct_contract(v: ContractsVisitor, n_signature: ASignature, n_annotations: Array[AAnnotation], mcontract: MContract, exist_contract: Bool)
do
- if check_same_contract(v, n_annotation, mcontract) then return
- if not exist_contract and not is_intro then no_intro_contract(v, n_signature, mcontract, n_annotation)
+ if not exist_contract and not is_intro then no_intro_contract(v, mcontract, n_annotations)
v.define_signature(mcontract, n_signature, mproperty.intro.msignature)
- var conditiondef = v.build_contract(n_annotation, mcontract, mclassdef)
+ v.build_contract(n_annotations, mcontract, mclassdef)
check_contract_facet(v, n_signature.clone, mclassdef, mcontract, exist_contract)
has_contract = true
end
# Create a contract on the introduction classdef of the property.
# Display an warning message if necessary
- private fun no_intro_contract(v: ContractsVisitor, n_signature: ASignature, mcontract: MContract, n_annotation: AAnnotation)
+ private fun no_intro_contract(v: ContractsVisitor, mcontract: MContract, n_annotations: Array[AAnnotation])
do
- mcontract.create_empty_contract(v, mcontract.intro_mclassdef, mcontract.adapt_msignature(self.mproperty.intro.msignature), mcontract.adapt_nsignature(n_signature))
- mcontract.no_intro_contract(v, n_annotation)
- mproperty.intro.has_contract = true
+ v.toolcontext.modelbuilder.create_method_from_property(mcontract, mcontract.intro_mclassdef, false, v.m_signature)
+ mcontract.no_intro_contract(v, n_annotations)
end
- # Is the contract already defined in the context
- #
- # Exemple :
- # fun foo is expect([...]), expect([...])
- #
- # 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
+ # Apply the `no_contract` annotation to the contract. This method removes the inheritance by adding an empty contract method.
+ # Display a warning if the annotation is not needed
+ private fun no_contract_apply(v: ContractsVisitor, n_signature: ASignature)
do
- if self.mclassdef.mpropdefs_by_property.has_key(mcontract) then
- v.toolcontext.error(n_annotation.location, "The method already has a defined `{mcontract.contract_name}` contract at line {self.mclassdef.mpropdefs_by_property[mcontract].location.line_start}")
- return true
+ var mensure = mproperty.mensure
+ var mexpect = mproperty.mexpect
+ if mensure == null and mexpect == null then
+ v.toolcontext.warning(location, "useless_nocontract", "Useless `no_contract`, no contract was declared for `{name}`. Remove the `no_contract`")
+ end
+ if mensure != null then
+ # Add an empty ensure method to replace the actual definition
+ v.toolcontext.modelbuilder.create_method_from_property(mensure, mclassdef, false, mensure.intro.msignature)
+ end
+ if mexpect != null then
+ # Add an empty expect method to replace the actual definition
+ v.toolcontext.modelbuilder.create_method_from_property(mexpect, mclassdef, false, mexpect.intro.msignature)
end
- return false
end
end
redef class APropdef
redef fun check_callsite(v)
do
- v.visited_method = self
+ v.visited_propdef = self
end
end
redef fun create_contracts(v)
do
v.ast_builder.check_mmodule(mpropdef.mclassdef.mmodule)
-
v.current_location = self.location
v.is_intro_contract = mpropdef.is_intro
+ check_annotation(v)
+ if not mpropdef.is_intro then check_redef(v)
+ end
- if n_annotations != null then
- for n_annotation in n_annotations.n_items do
- check_annotation(v,n_annotation)
- end
+ # Verification of the annotation to know if it is a contract annotation.
+ # If this is the case, we built the appropriate contract.
+ private fun check_annotation(v: ContractsVisitor)
+ do
+ var annotations_expect = get_annotations("expect")
+ var annotations_ensure = get_annotations("ensure")
+ var annotation_no_contract = get_annotations("no_contract")
+
+ if (not annotations_expect.is_empty or not annotations_ensure.is_empty) and not annotation_no_contract.is_empty then
+ v.toolcontext.error(location, "The new contract definition is not correct when using `no_contract`. Remove the contract definition or the `no_contract`")
+ return
end
- if not mpropdef.is_intro and not v.find_no_contract then
- self.check_redef(v)
+ var nsignature = n_signature or else new ASignature
+
+ if not annotation_no_contract.is_empty then
+ mpropdef.no_contract_apply(v, nsignature.clone)
+ return
end
- # reset the flag
- v.find_no_contract = false
- end
+ if not annotations_expect.is_empty then
+ var exist_contract = mpropdef.mproperty.has_expect
+ mpropdef.construct_contract(v, nsignature.clone, annotations_expect, mpropdef.mproperty.build_expect, exist_contract)
+ end
- # Verification of the annotation to know if it is a contract annotation.
- # If this is the case, we built the appropriate contract.
- private fun check_annotation(v: ContractsVisitor, n_annotation: AAnnotation)
- do
- 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 == "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
- # no_contract found set the flag to true
- v.find_no_contract = true
+ if not annotations_ensure.is_empty then
+ var exist_contract = mpropdef.mproperty.has_ensure
+ mpropdef.construct_contract(v, nsignature.clone, annotations_ensure, mpropdef.mproperty.build_ensure, exist_contract)
end
end
redef class MSignature
- # Adapt signature for a expect condition
- # Removed the return type is it not necessary
- private fun adapt_to_condition: MSignature do return new MSignature(mparameters.to_a, null)
+ # Adapt signature for an contract
+ #
+ # The returned `MSignature` is the copy of `self` without return type.
+ private fun adapt_to_contract: MSignature do return new MSignature(mparameters.to_a, null)
- # Adapt signature for a ensure condition
+ # Adapt signature for a ensure contract
#
- # Create new parameter with the return type
+ # The returned `MSignature` is the copy of `self` without return type.
+ # The return type is replaced by a new parameter `result`
private fun adapt_to_ensurecondition: MSignature
do
var rtype = return_mtype
- var msignature = adapt_to_condition
+ var msignature = adapt_to_contract
if rtype != null then
msignature.mparameters.add(new MParameter("result", rtype, false))
end
return msignature
end
- # Adapt signature for a expect condition
- # Removed the return type is it not necessary
+ # The returned `MSignature` is the exact copy of `self`.
private fun clone: MSignature do return new MSignature(mparameters.to_a, return_mtype)
end
return args
end
- # Return a copy of self adapted for the expect condition
- # npropdef it is use to define the parent of the parameters
- private fun adapt_to_condition(return_type: nullable AType): ASignature
+ # Create a new ASignature adapted for contract
+ #
+ # The returned `ASignature` is the copy of `self` without return type.
+ private fun adapt_to_contract: ASignature
do
var adapt_nsignature = self.clone
- adapt_nsignature.n_type = return_type
+ if adapt_nsignature.n_type != null then adapt_nsignature.n_type.detach
return adapt_nsignature
end
- # Return a copy of self adapted for postcondition on npropdef
+ # Create a new ASignature adapted for ensure
+ #
+ # The returned `ASignature` is the copy of `self` without return type.
+ # The return type is replaced by a new parameter `result`
private fun adapt_to_ensurecondition: ASignature do
- var nsignature = adapt_to_condition(null)
+ var nsignature = adapt_to_contract
if ret_type != null then
- var n_id = new TId
- n_id.text = "result"
- var new_param = new AParam
- new_param.n_id = n_id
- new_param.variable = new Variable(n_id.text)
- new_param.variable.declared_type = ret_type
- nsignature.n_params.add new_param
+ var variable = new Variable("result")
+ variable.declared_type = ret_type
+ nsignature.n_params.add new AParam.make(variable, ret_type.create_ast_representation)
end
return nsignature
end