static-analysis - sast - sonarqube vs fortify

¿Debería el verificador estático de Contratos de código ser capaz de verificar el límite aritmético?

Question

(También publicado en el foro de MSDN , pero eso no genera mucho tráfico, por lo que puedo ver).

He estado tratando de dar un ejemplo de Assert and Assume . Aquí está el código que tengo:

public static int RollDice(Random rng)
{
Contract.Ensures(Contract.Result<int>() >= 2 &&
Contract.Result<int>() <= 12);
if (rng == null)
{
rng = new Random();
}
Contract.Assert(rng != null);
int firstRoll = rng.Next(1, 7);
Contract.Assume(firstRoll >= 1 && firstRoll <= 6);
int secondRoll = rng.Next(1, 7);
Contract.Assume(secondRoll >= 1 && secondRoll <= 6);
return firstRoll + secondRoll;
}

(El asunto de poder pasar una referencia nula en lugar de una referencia Random existente es puramente pedagógico, por supuesto).

Tenía la esperanza de que si el corrector sabía que firstRoll y secondRoll estaban cada uno en el rango [1, 6] , podría calcular que la suma estaba en el rango [2, 12] .

¿Es esto una esperanza irracional? Me doy cuenta de que es un asunto complicado, averiguar exactamente qué podría pasar ... pero esperaba que el inspector fuera lo suficientemente inteligente :)

Si esto no es compatible ahora, ¿alguien sabe aquí si es probable que sea compatible en un futuro cercano?

EDITAR: Ahora he encontrado que hay opciones muy complicadas para la aritmética en el comprobador estático. Usando el cuadro de texto "avanzado" puedo probarlos desde Visual Studio, pero no hay una explicación decente de lo que hacen, hasta donde sé.

Answer 1

He tenido una respuesta en el foro de MSDN. Resulta que estaba muy cerca de allí. Básicamente, el verificador estático funciona mejor si se dividen los contratos "editados". Entonces, si cambiamos el código a esto:

public static int RollDice(Random rng)
{
Contract.Ensures(Contract.Result<int>() >= 2);
Contract.Ensures(Contract.Result<int>() <= 12);
if (rng == null)
{
rng = new Random();
}
Contract.Assert(rng != null);
int firstRoll = rng.Next(1, 7);
Contract.Assume(firstRoll >= 1);
Contract.Assume(firstRoll <= 6);
int secondRoll = rng.Next(1, 7);
Contract.Assume(secondRoll >= 1);
Contract.Assume(secondRoll <= 6);
return firstRoll + secondRoll;
}

Eso funciona sin ningún problema. También significa que el ejemplo es aún más útil, ya que resalta el punto de que el verificador funciona mejor con contratos separados.

Answer 2

No conozco la herramienta MS Contracts Checker, pero el análisis de rango es una técnica estándar de análisis estático; es ampliamente utilizado en herramientas comerciales de análisis estático para verificar que las expresiones de subíndices sean legales.

MS Research tiene una buena trayectoria en este tipo de análisis estático, por lo que espero que el análisis de rango sea un objetivo del Contracts Checker, incluso si no se comprueba actualmente.