diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-24 14:33:57 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-24 14:33:57 +0200 |
| commit | 9a8fcdd29d763d2b5650166ddd5b359a8bfed373 (patch) | |
| tree | 7675895f88b344e88ce0263cf1faf52daece73d7 | |
| parent | 3c8429b030efcaba205b8d0faf7fdd1f174ea1e7 (diff) | |
| download | compcert-kvx-9a8fcdd29d763d2b5650166ddd5b359a8bfed373.tar.gz compcert-kvx-9a8fcdd29d763d2b5650166ddd5b359a8bfed373.zip | |
trace quand le simulateur est appele
| -rw-r--r-- | kvx/lib/RTLpathSE_impl_junk.v | 5 | ||||
| -rw-r--r-- | test/c/Makefile | 2 | ||||
| -rw-r--r-- | test/regression/Makefile | 2 |
3 files changed, 6 insertions, 3 deletions
diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v index e82cca10..1b4efad7 100644 --- a/kvx/lib/RTLpathSE_impl_junk.v +++ b/kvx/lib/RTLpathSE_impl_junk.v @@ -678,8 +678,9 @@ Qed. Global Opaque simu_check_rec. Global Hint Resolve simu_check_rec_correct: wlp. -Definition imp_simu_check (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function): ?? unit := - simu_check_rec dm f tf (PTree.elements dm). +Definition imp_simu_check (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function): ?? unit := + simu_check_rec dm f tf (PTree.elements dm);; + println("simu_check OK!"). Local Hint Resolve PTree.elements_correct: core. Lemma imp_simu_check_correct dm f tf: diff --git a/test/c/Makefile b/test/c/Makefile index 726631d2..a728d182 100644 --- a/test/c/Makefile +++ b/test/c/Makefile @@ -1,6 +1,8 @@ include ../../Makefile.config CCOMP=../../ccomp +# TODO - temporary +# CCOMPOPTS:=$(CCOMPOPTS) -fall-loads-nontrap -fduplicate 2 -fprepass CCOMPFLAGS=$(CCOMPOPTS) -stdlib ../../runtime -dc -dclight -dasm CFLAGS+=-O2 -Wall diff --git a/test/regression/Makefile b/test/regression/Makefile index 87827282..8b2f4021 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -2,7 +2,7 @@ include ../../Makefile.config CCOMP=../../ccomp # TODO - temporary -CCOMPOPTS:=$(CCOMPOPTS) -fall-loads-nontrap -fduplicate 2 -fprepass +# CCOMPOPTS:=$(CCOMPOPTS) -fall-loads-nontrap -fduplicate 2 -fprepass CCOMPFLAGS=$(CCOMPOPTS) -stdlib ../../runtime \ -dparse -dc -dclight -dasm -fall \ -DARCH_$(ARCH) -DMODEL_$(MODEL) |