Ложное срабатывание: предварительное условие избыточно

Почему я получаю следующее предупреждение для этого тривиального примера кода, как только уровень предупреждения находится на уровне 2 или выше?

public int Foo(int a)
{
    if (a >= 0) throw new ArgumentException("a should be negative", "a");
    Contract.EndContractBlock();
    return a;
}

CodeContracts: Предлагаемые требования: Это предварительное условие является избыточным: рассмотрите возможность его удаления. Вы сравниваете значение структуры с нулевым?

Ясно, что целое число может быть отрицательным, поэтому предусловие вряд ли излишне, так почему же я получаю это предупреждение?

Изменить: вот что показывает ILSpy для созданной функции при просмотре исполняемого файла:

public int Foo(int a)
{
    if (a >= 0)
    {
        ContractHelper.RaiseContractFailedEvent(ContractFailureKind.Precondition, null, "a < 0", null);
        throw new ArgumentException("a should be negative", "a");
    }
    return a;
}

Настройки кодовых контрактов


person Voo    schedule 18.06.2015    source источник
comment
Где вы используете b в функции?   -  person lakshayg    schedule 18.06.2015
comment
@Lakshay Совсем не в этой урезанной версии. Но его удаление не удаляет предложение. Просто проглядел это при создании минимального примера, убрал.   -  person Voo    schedule 18.06.2015
comment
Вы уверены, что это точный код? Может ли быть так, что сравнение выполняется, например, для целого числа без знака? Можете ли вы проверить IL, который это генерирует?   -  person Luaan    schedule 18.06.2015
comment
@Luaan Я могу скопировать точный код, показанный здесь, в свой проект VS 2013 с Code Contracts и получить это предупреждение при сборке. Режим сборки — это проверка настраиваемых параметров, которая необходима при использовании версии контрактов кода backcomp if-then-throw, насколько я понимаю (в противном случае я получаю предупреждение о том, что он не поддерживается без этого режима и что он будет обрабатываться как Require ).   -  person Voo    schedule 18.06.2015
comment
Это происходит, когда вы делаете 0 <= a ? clt обычно используется для as и is в режиме выпуска. Можете ли вы проверить, отличается ли он и для выпуска/отладки?   -  person leppie    schedule 18.06.2015
comment
На заметку: разве это не должно быть ArgumentOutOfRangeException?   -  person CSharpie    schedule 18.06.2015
comment
@leppie Ничего не меняет. Сгенерированный IL равен ldarg.1; ldc.i4.0; clt для первой версии (перевернутый и cgt для второй), так что ничего необычного я бы не сказал.   -  person Voo    schedule 18.06.2015
comment
@Voo: анализатор IL должен иметь ошибку IMO. Чтобы обойти это, проверьте бит знака или что-то в этом роде.   -  person leppie    schedule 18.06.2015
comment
Я не понимаю этого предупреждения. Каковы ваши настройки контрактов кода и какую версию вы используете? (я использую 1.7.11202.10)   -  person Matthew Watson    schedule 18.06.2015
comment
@Matthew Интересно, только что сегодня скачал новейшую версию (кажется, то же самое) и запустил профессиональное обновление 4 VS 2013. Может быть, мне следует создать новое решение, чтобы увидеть, не в этом ли проблема. На всякий случай я добавил скриншот со страницы настроек кодовых контрактов. Редактировать: только что вспомнил, что я немного увеличил уровень предупреждения, потому что раньше играл с Contract.Assert, так что, вероятно, это как-то связано с этим.   -  person Voo    schedule 18.06.2015
comment
Какой уровень предупреждения? Вы получаете это предупреждение во время проверки статического контракта? Кроме того, отлаживать или выпускать сборку? (кстати, я использую тот же VS, что и вы)   -  person Matthew Watson    schedule 18.06.2015
comment
@Matthew Это отладочная сборка с любым процессором, статической проверкой контрактов, полной проверкой контрактов во время выполнения и соответствующими предупреждениями (второе слева). На изображении показаны мои точные настройки, которые я использую, чтобы получить сообщение об ошибке, если вам нужна дополнительная информация.   -  person Voo    schedule 18.06.2015
comment
Я могу воспроизвести это тоже сейчас.   -  person Matthew Watson    schedule 18.06.2015
comment
Я также отмечаю, что Contract.Requires(a < 0); не выдает предупреждения.   -  person Matthew Watson    schedule 18.06.2015
comment
Я думаю, вам следует опубликовать это как проблему здесь: github.com/Microsoft/CodeContracts   -  person Matthew Watson    schedule 18.06.2015
comment
@Matthew Да, похоже, это ошибка, а не просто неправильная конфигурация или непонимание с моей стороны. Сделаю сегодня вечером (ака несколько часов). Спасибо за вашу помощь.   -  person Voo    schedule 18.06.2015
comment
ошибка GitHub.   -  person Voo    schedule 18.06.2015
comment
Я предполагаю, что вы стали жертвой автоматического вывода необходимых предварительных условий. См. раздел 6.6.4 справочного руководства по контрактам кода под названием «Вывод». Вероятно, a ‹ 0 автоматически распространяется вызывающим абонентам, поэтому указывать его по буквам излишне.   -  person Mystra007    schedule 18.06.2015
comment
Для справки, в руководстве также говорится о избыточных предположениях: включение этой опции заставляет средство проверки пытаться доказать утверждения Contract.Assume и предупреждать, если они доказуемы. Мы предлагаем вам использовать эту опцию только изредка, чтобы избавиться от избыточных предположений, но не постоянно, так как это существенно замедляет статический анализ. Итак, мой вывод заключается в том, что проверенные вами параметры: infer требует и проверяет избыточные условные выражения, выдает это предупреждение, потому что контракты кода выяснили ограничение...   -  person Mystra007    schedule 18.06.2015
comment
@Mystra Интересная идея, завтра проверю. Странно, что это настройка по умолчанию в VS, учитывая данное руководство.   -  person Voo    schedule 18.06.2015


Ответы (1)


Я знаю, что это не дает прямого ответа на ваш вопрос, но, похоже, вы используете устаревший режим для кодовых контрактов.

В этом документе описывается рекомендуемый режим сборки, основанный на требованиях к использованию:

http://research.microsoft.com/en-us/projects/contracts/userdoc.pdf

Со страниц 20, 21...

рекомендации по использованию режима сборки

Еще один фрагмент из документа:

5.1.1 Режим сборки

Инструменты контракта должны знать, какой режим использования вы выберете. Если вы используете VisualStudio, выберите режим сборки на панели свойств контракта следующим образом:

  • Использование 1 или 2: требуется стандартный контракт
  • Использование 3: Проверка пользовательского параметра

Это позволяет инструментам выдавать надлежащие предупреждения, когда вы нарушаете правила использования. Если вы используете инструменты из командной строки, передайте правильный аргумент для параметра -assemblyMode.

Таким образом, используя режим сборки Standard Contract Requires, вы можете сделать одно из следующих действий:

Contract.Requires<ArgumentException>(a < 0, "a");
// OR
Contract.Requires(a < 0, "a should be negative");

Ни один из них не генерирует никаких предупреждений для меня.

Я надеюсь, что это поможет в любом случае.

Ура питески

person peteski    schedule 09.07.2015