c# - unitarios - "Invariante no probado" cuando se usa un método que crea un nuevo objeto específico en su declaración de devolución

test in c#

Question

El siguiente código simple producirá una advertencia "invariante no comprobada" por el verificador estático de los Contratos de Código, aunque no hay forma de que _foo pueda ser null . La advertencia es para la declaración de return dentro de UncalledMethod .

public class Node
{
public Node(string s1, string s2, string s3, string s4, object o,
string s5)
{
}
}
public class Bar
{
private readonly string _foo;
public Bar()
{
_foo = "foo";
}
private object UncalledMethod()
{
return new Node(string.Empty, string.Empty, string.Empty, string.Empty,
GetNode(), string.Empty);
}
private Node GetNode()
{
return null;
}
public string Foo
{
get
{
Contract.Ensures(Contract.Result<string>() != null);
return _foo;
}
}
[ContractInvariantMethod]
private void Invariants()
{
Contract.Invariant(_foo != null);
}
}

Aparte del hecho de que la advertencia es simplemente inválida, solo ocurre en ciertas circunstancias específicas. Cambiar cualquiera de lo siguiente hará que la advertencia desaparezca:

1. Inline GetNode lo que la declaración de retorno se ve así:

   return new Node(string.Empty, string.Empty, string.Empty, string.Empty, null,
   string.Empty);

2. Elimine cualquiera de los parámetros s1 a s5 del constructor de Node .
3. Cambie el tipo de cualquiera de los parámetros s1 a s5 del constructor de Node a object .

4. Use una variable temporal para el resultado de GetNode :

    var node = GetNode();
   return new Node(string.Empty, string.Empty, string.Empty, string.Empty,
   node, string.Empty);

5. Cambiando el orden de los parámetros del constructor de Node .
6. Verificando la opción "Mostrar suposiciones" en el panel de configuración de contratos de código en la configuración del proyecto.

¿Me estoy perdiendo algo obvio aquí o es simplemente un error en el comprobador estático?

Mi configuración:

Mi salida:

C:/{path}/Program.cs(20,9): message : CodeContracts: Suggested ensures: Contract.Ensures(this._foo != null);
C:/{path}/Program.cs(41,17): message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.Result<System.String>() == this._foo);
C:/{path}/Program.cs(33,13): message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.Result<ConsoleApplication3.Program+Node>() == null);
C:/{path}/Program.cs(27,13): message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.Result<System.Object>() != null);
C:/{path}/Program.cs(55,13): message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.ForAll(0, args.Length, __k__ => args[__k__] != 0));
CodeContracts: ConsoleApplication3: Validated: 92,3%
CodeContracts: ConsoleApplication3: Contract density: 1,81
CodeContracts: ConsoleApplication3: Total methods analyzed 8
CodeContracts: ConsoleApplication3: Methods with 0 warnings 7
CodeContracts: ConsoleApplication3: Total method analysis read from the cache 8
CodeContracts: ConsoleApplication3: Total time 2,522sec. 315ms/method
CodeContracts: ConsoleApplication3: Retained 0 preconditions after filtering
CodeContracts: ConsoleApplication3: Inferred 0 object invariants
CodeContracts: ConsoleApplication3: Retained 0 object invariants after filtering
CodeContracts: ConsoleApplication3: Detected 0 code fixes
CodeContracts: ConsoleApplication3: Proof obligations with a code fix: 0
C:/{path}/Program.cs(27,13): warning : CodeContracts: invariant unproven: _foo != null
C:/{path}/Program.cs(49,13): warning : + location related to previous warning
C:/windows/system32/ConsoleApplication3.exe(1,1): message : CodeContracts: Checked 13 assertions: 12 correct 1 unknown
CodeContracts: ConsoleApplication3:
CodeContracts: ConsoleApplication3: Background contract analysis done.

Answer 1

Esto ya no es un problema con la última versión .