¿Alternativa de código abierto para Mathworks Polyspace?

Question

¿Alguien sabe acerca de un proyecto de código abierto (o tal vez solo de uso gratuito en proyectos comerciales) que es una alternativa al Mathworks Polyspace?

Estoy buscando herramientas para la verificación de código y encontré algunas buenas alternativas para las comprobaciones estáticas, pero PolySpace parece ofrecer mucha más potencia. Creo que no hay una alternativa real, pero tal vez usted lo sepa mejor. :)

a lo solicitado (lo siento, por el retraso, RL se pone al día ...) añado mis idiomas preferidos para esta herramienta:

1. Java
2. .NET (estaré bien con C# solamente)
3. C/C++ (no es un must-have)

Answer 1

Polyspace solo maneja C, C++ y Java, por lo que es una poderosa alternativa de hecho que usted está buscando. La búsqueda dinámica de métodos que está presente en C# y Java no hace que estos lenguajes sean más fáciles de analizar.

Para C, echar un vistazo a http://frama-c.cea.fr/

Answer 2

Polyspace está diseñado en torno a algunos muy sofisticada tecnología de análisis de programa. No creo que veas versiones de código abierto/libre de esto en el corto plazo.

Answer 3

Sé que esto es cuestión de edad, pero hay un montón de herramientas por lo que si usted está interesado en el análisis de código estático aquí se list of tools ordenados por idioma.

Si nos fijamos sólo para herramienta de código abierto para el código Java le recomiendo que FindBugs

Answer 4

para C/C++ existe Klee, lo que parece bastante cerca de PolySpace http://klee.llvm.org

Klee es una herramienta que es el resultado de un proyecto de investigación, y le permite realizar la ejecución simbólica de un programa C/C++ compilándolo en un bytecode LLVM y ejecutándolo con un intérprete personalizado. Esto permite la detección de errores de tiempo de ejecución, como desbordamientos de búfer, división por cero y sobrecambio, y cuando encuentra un error de este tipo escribe un caso de prueba para reproducirlo y ver para qué valores ocurrió el error. Originalmente escrito para utilidades de línea de comando estándar, puede usarse también para un programa genérico, al hacer que su entrada sea simbólica (la estoy probando en el firmware incorporado). ¡Espero que esto ayude!