From ab6d5e98b4d967cc7834ad457b36bbf4c141f2ee Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 15 Aug 2017 11:54:51 +0200 Subject: 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. --- Changelog | 1 + 1 file changed, 1 insertion(+) (limited to 'Changelog') diff --git a/Changelog b/Changelog index a7946db5..a8cb6d22 100644 --- a/Changelog +++ b/Changelog @@ -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 -- cgit