El lenguaje C sigue siendo una pieza central de la infraestructura informática, pero su definición formal —el estándar ISO— se ha distanciado tanto de las propiedades que el código de sistemas asume como de las que los compiladores implementan, y ninguna de esas visiones está claramente caracterizada. Este artículo aborda esa brecha con dos aportaciones. La primera es un análisis en profundidad del espacio de diseño de la semántica de punteros y memoria en el C usado en la práctica: plantea preguntas concretas, construye una suite de casos de prueba semánticos, recoge datos experimentales de varias implementaciones y encuesta las creencias de expertos en C, identificando consensos (coincidentes con ISO o divergentes) y conflictos. Todo ello se aplica a un C experimental implementado sobre hardware con capacidades de memoria. La segunda aportación es Cerberus, un modelo formal para gran parte de C. Cerberus se parametriza sobre el modelo de memoria: puede enlazarse con un modelo de objetos de memoria de facto en construcción o con un modelo operacional de concurrencia C11; se define por elaboración hacia un lenguaje Core mucho más simple, lo que facilita su accesibilidad, y es ejecutable como oráculo de pruebas en ejemplos pequeños. El trabajo busca ofrecer una base sólida para discutir qué es hoy el C convencional —qué pueden asumir programadores y herramientas de análisis y qué buscan implementar los compiladores— y avanzar hacia semánticas claras, consistentes y aceptadas para los distintos casos de uso del lenguaje.
