From 0813e36329cf88e8903de8f02abe5a616c3c49bd Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.maroneze@cea.fr> Date: Tue, 8 Dec 2020 18:04:01 +0100 Subject: [PATCH] [wp] rename test from .h to .i to ensure it is executed --- .../wp/tests/wp_plugin/{bitmask0x8000.h => bitmask0x8000.i} | 0 .../wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.res.oracle | 2 +- 2 files changed, 1 insertion(+), 1 deletion(-) rename src/plugins/wp/tests/wp_plugin/{bitmask0x8000.h => bitmask0x8000.i} (100%) diff --git a/src/plugins/wp/tests/wp_plugin/bitmask0x8000.h b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i similarity index 100% rename from src/plugins/wp/tests/wp_plugin/bitmask0x8000.h rename to src/plugins/wp/tests/wp_plugin/bitmask0x8000.i diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.res.oracle index 1fdbf733859..5c4ea808416 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.res.oracle @@ -1,5 +1,5 @@ # frama-c -wp [...] -[kernel] Parsing tests/wp_plugin/bitmask0x8000.h (with preprocessing) +[kernel] Parsing tests/wp_plugin/bitmask0x8000.i (no preprocessing) [wp] Running WP plugin... [wp] 2 goals scheduled [wp] [Script] Goal typed_lemma_res_n : Valid -- GitLab