Mentions légales du service

Skip to content

Start conversion of RAC exec log to CE model

Benedikt Becker requested to merge convert-exec-trace-to-ce-model into master

This is specifically intended to provide RAC-verified CE models to Spark, where there is no easy way to display execution logs. There might still be changes required for the integration, but I would prefer to tackle them after this basic version has been merged.

This MR also adds

  • environment variables WHY3PRINTORIGINALMODEL and WHY3PRINTDERIVEDMODEL for why3 prove --check-ce to additionally print the original and derived models for comparison
  • changes required for the integration of Why3 check-ce to Spark
Edited by Benedikt Becker

Merge request reports