Strenghten postcondition and ccrewrite

Question

I have reviewed previous problems with ccrewrite but haven't found this concrete issue. 

I define some preconditions for an interface, and add a postcondition in a given implemented class for that interface. ccrewrite exits with -1 code.

In code:

 [ContractClass(typeof(ICalculateContract))]
    public interface ICalculate
    {
        float Calculate(Dictionary<string, float> dict);
    }

    [ContractClassFor(typeof(ICalculate))]
    public abstract class ICalculateContract : ICalculate
    {
        public float Calculate(Dictionary<string, float> dict)
        {
            Contract.Requires<ArgumentNullException>(dict != null);
            Contract.Requires<ArgumentException>(Contract.ForAll(dict, item => item.Value > 0));
            throw new NotImplementedException();
        }
    }

    public class CalculateNode : ICalculate
    {
        private string _name;
        private string _ensures;

        public CalculateNode(string ensures, string name)
        {
            _name = name;
            _ensures = ensures;
        }

        [ContractInvariantMethod]
        private void Invariant()
        {
            Contract.Invariant(!string.IsNullOrEmpty(_name));
            Contract.Invariant(!string.IsNullOrEmpty(_ensures));
        }

        public float Calculate(Dictionary<string, float> dict)
        {
            Contract.Ensures(Contract.Exists(dict, item => item.Key == _ensures));
            return 5f;
        }
    }

If I put all PRE and POST in the implemented class, it is able to rewrite, although static check adds a warning as expected because preconditions are being added in an inherited class.

Context:

Contracts: v1.4.51019.0, VStudio 2012 Premium 11.0.51106.01 Update 1, 

Runtime and static checking.

Answer 1

Hello,

  can you try with the latest version? I just tried your example, and I got no problem from the rewriter.

ciao

f

Answer 2

Same error with 1.4.60218.0 version. I add code contracts project configuration in order to make the context cloned:

Answer 3

I tried this morning, but I cannot repro this problem.

Do you have more info about what you have installed/not installed on your machine ? 4.0 vs 4.5 vs2010 vs2012, etc? Can you try again with the latest installer?

-MaF

---

Cheers, -MaF (Manuel Fahndrich)