aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Frontend.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2020-04-16 20:23:35 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2020-04-20 13:30:03 +0200
commit438d541dbe5fe7d7fe6b7aacaa6e6ef070c2e237 (patch)
treef2ca20b3130b302bdaf3841d6105c8138dd48583 /driver/Frontend.ml
parent0a2db0269809539ccc66f8ec73637c37fbd23580 (diff)
downloadcompcert-kvx-438d541dbe5fe7d7fe6b7aacaa6e6ef070c2e237.tar.gz
compcert-kvx-438d541dbe5fe7d7fe6b7aacaa6e6ef070c2e237.zip
Move reserved_registers to CPragmas.
The list of reserved_registers is never reset between the compilation of multiple files. Instead of storing them in IRC they are moved in the CPragmas file and reset in the a new reset function for Cpragmas whic is called per file.
Diffstat (limited to 'driver/Frontend.ml')
-rw-r--r--driver/Frontend.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index 74791247..bb97e945 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -75,6 +75,7 @@ let preprocess ifile ofile =
let parse_c_file sourcename ifile =
Debug.init_compile_unit sourcename;
Sections.initialize();
+ CPragmas.reset();
(* Simplification options *)
let simplifs =
"b" (* blocks: mandatory *)