diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-03-10 14:13:19 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-10 14:13:19 +0100 |
| commit | 163f4a4e4467f64759dfa67bd555e6b893692561 (patch) | |
| tree | 81731eb1f0e6bdc6c1fc321d0b865bb056eef5cc | |
| parent | c68661bd1eb5565e1272e039d7c2fa34086abf90 (diff) | |
| download | compcert-kvx-vericert.tar.gz compcert-kvx-vericert.zip | |
Compile under the name: kvxvericert
| -rw-r--r-- | Makefile | 8 | ||||
| -rw-r--r-- | lib/Floats.v | 2 | ||||
| -rw-r--r-- | lib/IEEE754_extra.v | 2 | ||||
| -rw-r--r-- | verilog/Archi.v | 2 |
4 files changed, 7 insertions, 7 deletions
@@ -36,18 +36,18 @@ DIRS := lib lib/Impure common $(ARCHDIRS) scheduling backend cfrontend driver \ RECDIRS:=lib common $(ARCHDIRS) scheduling backend cfrontend driver flocq exportclight \ cparser -COQINCLUDES := $(foreach d, $(DIRS), -R $(d) compcert.$(subst /,.,$d)) +COQINCLUDES := $(foreach d, $(DIRS), -R $(d) kvx.$(subst /,.,$d)) ifeq ($(LIBRARY_FLOCQ),local) DIRS += flocq/Core flocq/Prop flocq/Calc flocq/IEEE754 RECDIRS += flocq -COQINCLUDES += -R flocq Flocq +COQINCLUDES += -R flocq kvx.Flocq endif ifeq ($(LIBRARY_MENHIRLIB),local) DIRS += MenhirLib RECDIRS += MenhirLib -COQINCLUDES += -R MenhirLib MenhirLib +COQINCLUDES += -R MenhirLib kvx.MenhirLib endif # Notes on silenced Coq warnings: @@ -402,7 +402,7 @@ check-admitted: $(FILES) @grep -w 'admit\|Admitted\|ADMITTED' $^ || echo "Nothing admitted." check-proof: $(FILES) - $(COQCHK) compcert.driver.Complements + $(COQCHK) kvx.driver.Complements print-includes: @echo $(COQINCLUDES) diff --git a/lib/Floats.v b/lib/Floats.v index b10b3392..6530b41c 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -18,7 +18,7 @@ (** Formalization of floating-point numbers, using the Flocq library. *) Require Import Coqlib Zbits Integers Axioms. -From Flocq Require Import Binary Bits Core. +From kvx.Flocq Require Import Binary Bits Core. Require Import IEEE754_extra. Require Import Program. Require Archi. diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index b0d1944e..fbcd527e 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -18,7 +18,7 @@ (** Additional operations and proofs about IEEE-754 binary floating-point numbers, on top of the Flocq library. *) -From Flocq Require Import Core Digits Operations Round Bracket Sterbenz +From kvx.Flocq Require Import Core Digits Operations Round Bracket Sterbenz Binary Round_odd. Require Import Psatz. Require Import Bool. diff --git a/verilog/Archi.v b/verilog/Archi.v index dc5a078d..aef813a4 100644 --- a/verilog/Archi.v +++ b/verilog/Archi.v @@ -17,7 +17,7 @@ (** Architecture-dependent parameters for x86 in 32-bit mode *) -From Flocq Require Import Binary Bits. +From kvx.Flocq Require Import Binary Bits. Require Import ZArith List. Definition ptr64 := false. |