diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-15 11:54:51 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-15 11:54:51 +0200 |
| commit | ab6d5e98b4d967cc7834ad457b36bbf4c141f2ee (patch) | |
| tree | 8797015ad9d75bbaf6fadcdd0c418d29020120ab /Changelog | |
| parent | 0aa08f5d521401644b5c839239de97f587e0a217 (diff) | |
| download | compcert-kvx-ab6d5e98b4d967cc7834ad457b36bbf4c141f2ee.tar.gz compcert-kvx-ab6d5e98b4d967cc7834ad457b36bbf4c141f2ee.zip | |
Issue #196: excessive proof-checking times in .v files generated by clightgen
The check that "build_composite_env composites = OK (make_composite_env composites)" is taking time exponential on the number of struct/union definitions, at least on the example provided in #196.
The solution implemented in this commit is to use computational reflection more efficiently, just to check that "build_composite_env composites" is of the form "OK _". From there, a new function Clightdefs.mkprogram produces the appropriate Clight.program without additional computation.
Diffstat (limited to 'Changelog')
| -rw-r--r-- | Changelog | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -24,6 +24,7 @@ Usability: Bug fixing: - Issue #179: clightgen produces wrong output for "switch" statements. +- Issue #196: excessive proof times in .v files produced by clightgen. - Do not generate code for functions with "inline" specifier that are neither static nor extern, as per ISO C99. - Some line number information was missing for some goto labels and |