aboutsummaryrefslogtreecommitdiffstats
path: root/configure
diff options
context:
space:
mode:
authorDavid Monniaux <David.Monniaux@univ-grenoble-alpes.fr>2022-02-12 12:06:32 +0100
committerDavid Monniaux <David.Monniaux@univ-grenoble-alpes.fr>2022-02-12 12:06:32 +0100
commit50377ef4b9430fa019e26fac3028739f0308e9b1 (patch)
tree4a2ce2c21c96f5ba04787f0d8bccb8bb8784d894 /configure
parent5ba8c76d3eaf78d1a57678af5d9b006e29c4a02f (diff)
downloadcompcert-kvx-50377ef4b9430fa019e26fac3028739f0308e9b1.tar.gz
compcert-kvx-50377ef4b9430fa019e26fac3028739f0308e9b1.zip
unsigned long -> float without function calls
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure1
1 files changed, 1 insertions, 0 deletions
diff --git a/configure b/configure
index 61a6697c..685ce390 100755
--- a/configure
+++ b/configure
@@ -821,6 +821,7 @@ CFLAGS= -D __KVX_COS__
SIMU=kvx-cluster --
BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\
Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v Asmblockprops.v\\
+ FPExtra.v \\
ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\
Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\
AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v