Git Product home page Git Product logo

ymherklotz / vericert Goto Github PK

View Code? Open in Web Editor NEW
85.0 12.0 5.0 23.34 MB

A formally verified high-level synthesis tool based on CompCert and written in Coq.

Home Page: https://vericert.ymhg.org

License: GNU General Public License v3.0

Makefile 0.27% Coq 84.39% Nix 0.07% OCaml 12.49% C 0.14% Shell 0.40% SystemVerilog 1.01% Standard ML 0.02% Python 0.11% Tcl 0.62% Dockerfile 0.03% C++ 0.05% R 0.05% Scheme 0.35%
high-level-synthesis coq

vericert's Issues

make error on macOS

When I try to build Vericert on macOS Monterey, there is a make error during step nix-shell.
error info is like:
截屏2023-07-03 21 41 30
I wonder what's the matter with this.

`make` failed 

[nix-shell:~/vms/tools/coqup]$ make -j8 
(cd lib/CompCert && ./configure x86_64-linux)
Testing assembler support for CFI directives... no
Testing linker support for '-no-pie' / '-nopie' option... yes, '-no-pie'
Testing Coq... version 8.10.2 -- good!
Testing OCaml... version 4.09.1 -- good!
Testing OCaml .opt compilers... yes
Testing Menhir... version 20190626 -- good!
Testing GNU make... version 4.2.1 (command 'make') -- good!

CompCert configuration:
    Target architecture........... x86
    Hardware model................ 64
    Application binary interface.. standard
    Endianness.................... little
    OS and development env........ linux
    C compiler.................... gcc -m64
    C preprocessor................ gcc
    Assembler..................... gcc
    Assembler supports CFI........ false
    Assembler for runtime lib..... gcc -m64 -c
    Linker........................ gcc
    Linker needs '-no-pie'........ true
    Math library.................. -lm
    Build command to use.......... make
    Binaries installed in......... /usr/local/bin
    Runtime library provided...... true
    Library files installed in.... /usr/local/lib/compcert
    Standard headers provided..... true
    Standard headers installed in. /usr/local/lib/compcert/include
    Coq development will not be installed
make -C lib/CompCert
make[1]: Entering directory '/Users/jcheng/vms/tools/coqup/lib/CompCert'
make[2]: Entering directory '/Users/jcheng/vms/tools/coqup/lib/CompCert'
Analyzing Coq dependencies
make[2]: Leaving directory '/Users/jcheng/vms/tools/coqup/lib/CompCert'
make proof
make[2]: Entering directory '/Users/jcheng/vms/tools/coqup/lib/CompCert'
COQC x86_64/Archi.v
COQC lib/Integers.v
COQC lib/Ordered.v
COQC lib/Floats.v
COQC lib/Heaps.v
COQC common/AST.v
COQC common/Linking.v
COQC common/Values.v
COQC cfrontend/Ctypes.v
COQC common/Memdata.v
COQC common/Switch.v
COQC backend/Registers.v
COQC common/Memtype.v
COQC common/Builtins0.v
COQC common/Memory.v
COQC x86/Builtins1.v
COQC common/Builtins.v
COQC common/Globalenvs.v
COQC cfrontend/Cop.v
COQC common/Events.v
COQC cfrontend/Csyntax.v
COQC cfrontend/Initializers.v
COQC backend/Kildall.v
COQC common/Smallstep.v
COQC common/Separation.v
COQC x86/Op.v
COQC common/Behaviors.v
COQC backend/Cminor.v
COQC cfrontend/Csem.v
COQC cfrontend/Clight.v
COQC cfrontend/SimplExpr.v
COQC cfrontend/ClightBigstep.v
COQC cfrontend/SimplLocals.v
COQC cfrontend/Ctyping.v
COQC cfrontend/Cstrategy.v
COQC cfrontend/Initializersproof.v
COQC common/Determinism.v
COQC cfrontend/SimplExprspec.v
COQC cfrontend/SimplLocalsproof.v
COQC cfrontend/Csharpminor.v
COQC backend/Cminortyping.v
COQC cfrontend/Cminorgen.v
COQC cfrontend/Cminorgenproof.v
COQC cfrontend/Cexec.v
COQC backend/CminorSel.v
COQC x86/Machregs.v
COQC backend/RTL.v
COQC x86/SelectOp.v
COQC backend/Locations.v
COQC backend/RTLgen.v
COQC backend/Inlining.v
COQC backend/Renumber.v
COQC backend/Liveness.v
COQC backend/ValueDomain.v
COQC backend/CSEdomain.v
COQC backend/Unusedglob.v
COQC cfrontend/SimplExprproof.v
COQC backend/RTLgenspec.v
COQC backend/Inliningspec.v
COQC backend/Renumberproof.v
COQC x86/CombineOp.v
COQC backend/Unusedglobproof.v
COQC backend/SplitLong.v
COQC x86/SelectOpproof.v
COQC x86/Conventions1.v
COQC x86/SelectLong.v
COQC x86/CombineOpproof.v
COQC backend/RTLgenproof.v
COQC backend/Conventions.v
COQC cfrontend/Cshmgen.v
COQC backend/Tailcall.v
COQC backend/RTLtyping.v
COQC backend/LTL.v
COQC cfrontend/Cshmgenproof.v
COQC backend/SplitLongproof.v
COQC backend/Tailcallproof.v
COQC backend/Tunneling.v
COQC backend/Linear.v
COQC backend/SelectDiv.v
COQC backend/Inliningproof.v
COQC backend/Allocation.v
COQC backend/Tunnelingproof.v
COQC backend/Lineartyping.v
COQC backend/Linearize.v
COQC backend/CleanupLabels.v
COQC backend/Debugvar.v
COQC backend/Bounds.v
COQC backend/Selection.v
COQC x86/ValueAOp.v
COQC backend/NeedDomain.v
COQC backend/Linearizeproof.v
COQC backend/CleanupLabelsproof.v
COQC backend/Debugvarproof.v
COQC x86/Stacklayout.v
COQC x86/SelectLongproof.v
COQC backend/Allocproof.v
COQC backend/ValueAnalysis.v
COQC x86/ConstpropOp.v
COQC backend/Mach.v
COQC x86/Asm.v
COQC x86/NeedOp.v
COQC backend/Stacking.v
COQC backend/SelectDivproof.v
COQC x86/Asmgen.v
COQC backend/Stackingproof.v
COQC backend/Constprop.v
COQC x86/ConstpropOpproof.v
COQC backend/CSE.v
COQC backend/Deadcode.v
COQC backend/Asmgenproof0.v
COQC backend/CSEproof.v
COQC backend/Deadcodeproof.v
COQC x86/Asmgenproof1.v
COQC backend/Selectionproof.v
COQC backend/Constpropproof.v
COQC x86/Asmgenproof.v
COQC driver/Compiler.v
COQC driver/Complements.v
make[2]: Leaving directory '/Users/jcheng/vms/tools/coqup/lib/CompCert'
make extraction
make[2]: Entering directory '/Users/jcheng/vms/tools/coqup/lib/CompCert'
rm -f extraction/*.ml extraction/*.mli
"coqtop"  -R lib compcert.lib  -R common compcert.common  -R x86_64 compcert.x86_64  -R x86 compcert.x86  -R backend compcert.backend  -R cfrontend compcert.cfrontend  -R driver compcert.driver  -R flocq compcert.flocq  -R exportclight compcert.exportclight  -R MenhirLib compcert.MenhirLib  -R cparser compcert.cparser -batch -load-vernac-source extraction/extraction.v
File "/Users/jcheng/vms/tools/coqup/lib/CompCert/extraction/extraction.v", line 160, characters 0-1084:
Warning: The extraction is currently set to bypass opacity, the following
opaque constant bodies have been accessed : solve_constraints_terminate.
 [extraction-opaque-accessed,extraction]
touch extraction/STAMP
make[2]: Leaving directory '/Users/jcheng/vms/tools/coqup/lib/CompCert'
make ccomp
make[2]: Entering directory '/Users/jcheng/vms/tools/coqup/lib/CompCert'
make -f Makefile.extr depend
(echo "stdlib_path=/usr/local/lib/compcert"; \
         echo "prepro=gcc"; \
         echo "linker=gcc"; \
         echo "asm=gcc"; \
 echo "prepro_options=-std=c99 -m64 -U__GNUC__ -E";\
 echo "asm_options=-m64 -c";\
 echo "linker_options=-m64 -no-pie";\
         echo "arch=x86"; \
         echo "model=64"; \
         echo "abi=standard"; \
         echo "endianness=little"; \
         echo "system=linux"; \
         echo "has_runtime_lib=true"; \
         echo "has_standard_headers=true"; \
         echo "asm_supports_cfi=false"; \
 echo "response_file_style=gnu";) \
        > compcert.ini
make[3]: Entering directory '/Users/jcheng/vms/tools/coqup/lib/CompCert'
Analyzing OCaml dependencies
make[3]: Leaving directory '/Users/jcheng/vms/tools/coqup/lib/CompCert'
make -f Makefile.extr ccomp
make[3]: Entering directory '/Users/jcheng/vms/tools/coqup/lib/CompCert'
OCAMLC   extraction/Datatypes.mli
OCAMLC   extraction/BinNums.mli
OCAMLC   extraction/Bool.mli
OCAMLC   extraction/EquivDec.mli
OCAMLC   extraction/BoolEqual.mli
OCAMLC   extraction/String0.mli
OCAMLC   extraction/Equalities.mli
OCAMLC   extraction/Specif.mli
OCAMLC   extraction/Memtype.mli
OCAMLC   extraction/DecidableClass.mli
OCAMLC   extraction/Cabs.mli
OCAMLC   extraction/UnionFind.mli
OCAMLC   extraction/Compopts.mli
OCAMLC   extraction/Compare_dec.mli
OCAMLC   extraction/Nat.mli
OCAMLOPT extraction/Datatypes.ml
OCAMLOPT extraction/BinNums.ml
OCAMLC   extraction/BinPosDef.mli
OCAMLC   extraction/List0.mli
OCAMLC   extraction/Archi.mli
OCAMLOPT extraction/Bool.ml
OCAMLC   extraction/Orders.mli
OCAMLOPT extraction/EquivDec.ml
OCAMLOPT extraction/BoolEqual.ml
OCAMLOPT extraction/String0.ml
OCAMLC   extraction/Errors.mli
OCAMLOPT extraction/Equalities.ml
OCAMLC   extraction/DecidableType.mli
OCAMLOPT extraction/Specif.ml
OCAMLOPT extraction/Memtype.ml
OCAMLC   extraction/Ring.mli
OCAMLC   extraction/PeanoNat.mli
OCAMLC   driver/Driveraux.mli
OCAMLOPT extraction/DecidableClass.ml
OCAMLOPT extraction/Cabs.ml
OCAMLC   cparser/pre_parser.mli
OCAMLC   cparser/Elab.mli
OCAMLOPT extraction/UnionFind.ml
OCAMLOPT extraction/Compopts.ml
OCAMLOPT extraction/Compare_dec.ml
OCAMLC   extraction/Mergesort.mli
OCAMLC   x86/CBuiltins.ml
OCAMLOPT extraction/Nat.ml
OCAMLOPT extraction/BinPosDef.ml
OCAMLC   extraction/BinPos.mli
OCAMLOPT extraction/List0.ml
OCAMLOPT extraction/Archi.ml
OCAMLOPT extraction/Orders.ml
OCAMLC   extraction/OrdersTac.mli
OCAMLOPT extraction/Errors.ml
OCAMLOPT extraction/DecidableType.ml
OCAMLC   extraction/FSetInterface.mli
OCAMLOPT extraction/PeanoNat.ml
OCAMLOPT extraction/Ring.ml
OCAMLOPT cparser/pre_parser.ml
OCAMLC   cparser/ErrorReports.mli
OCAMLOPT cparser/Cabshelper.ml
OCAMLOPT extraction/BinPos.ml
OCAMLC   extraction/Zpower.mli
OCAMLC   extraction/BinNat.mli
OCAMLC   extraction/Digits.mli
OCAMLOPT extraction/OrdersTac.ml
OCAMLC   extraction/OrderedType.mli
OCAMLC   extraction/OrdersFacts.mli
OCAMLOPT extraction/FSetInterface.ml
OCAMLOPT x86/CBuiltins.ml
OCAMLOPT extraction/Mergesort.ml
OCAMLC   extraction/BinInt.mli
OCAMLC   extraction/OrdersAlt.mli
OCAMLC   extraction/MSetInterface.mli
OCAMLC   extraction/Alphabet.mli
OCAMLC   extraction/FMapList.mli
OCAMLOPT extraction/Zpower.ml
OCAMLOPT extraction/BinNat.ml
OCAMLC   extraction/ZArith_dec.mli
OCAMLC   extraction/Zaux.mli
OCAMLC   extraction/Zbool.mli
OCAMLC   extraction/FLT.mli
OCAMLOPT extraction/Digits.ml
OCAMLOPT extraction/OrderedType.ml
OCAMLOPT extraction/OrdersFacts.ml
OCAMLC   extraction/Int0.mli
OCAMLC   extraction/Znumtheory.mli
OCAMLC   extraction/Decidableplus.mli
OCAMLC   extraction/Grammar.mli
OCAMLOPT extraction/BinInt.ml
OCAMLC   extraction/Coqlib.mli
OCAMLC   extraction/Bracket.mli
OCAMLC   extraction/MSetAVL.mli
OCAMLC   extraction/FMapAVL.mli
OCAMLOPT extraction/OrdersAlt.ml
OCAMLOPT extraction/Alphabet.ml
OCAMLC   extraction/Automaton.mli
OCAMLOPT extraction/FMapList.ml
OCAMLC   extraction/IntvSets.mli
OCAMLC   extraction/FSetAVLplus.mli
OCAMLC   extraction/Zbits.mli
OCAMLC   extraction/Round.mli
OCAMLC   extraction/Maps.mli
OCAMLOPT extraction/MSetInterface.ml
OCAMLC   extraction/FSetAVL.mli
OCAMLC   extraction/Iteration.mli
OCAMLOPT extraction/Znumtheory.ml
OCAMLOPT extraction/Decidableplus.ml
OCAMLOPT extraction/Grammar.ml
OCAMLC   extraction/Interpreter_correct.mli
OCAMLC   extraction/Validator_safe.mli
OCAMLC   extraction/Postorder.mli
OCAMLOPT extraction/ZArith_dec.ml
OCAMLC   extraction/Integers.mli
OCAMLOPT extraction/Zaux.ml
OCAMLOPT extraction/Zbool.ml
OCAMLOPT extraction/FLT.ml
OCAMLC   extraction/Binary.mli
OCAMLC   extraction/Ordered.mli
OCAMLOPT extraction/Int0.ml
OCAMLC   extraction/Lattice.mli
OCAMLC   extraction/Unityping.mli
OCAMLOPT extraction/Automaton.ml
OCAMLC   extraction/Interpreter.mli
OCAMLC   extraction/Switch.mli
OCAMLOPT extraction/Bracket.ml
OCAMLOPT extraction/Coqlib.ml
OCAMLC   extraction/IEEE754_extra.mli
OCAMLOPT extraction/MSetAVL.ml
OCAMLC   extraction/Bits.mli
OCAMLC   extraction/Registers.mli
OCAMLC   extraction/Heaps.mli
OCAMLOPT extraction/Interpreter_correct.ml
OCAMLOPT extraction/Validator_safe.ml
OCAMLOPT extraction/IntvSets.ml
OCAMLOPT extraction/Zbits.ml
OCAMLOPT extraction/Round.ml
OCAMLC   extraction/Floats.mli
OCAMLOPT extraction/Maps.ml
OCAMLOPT extraction/Iteration.ml
OCAMLC   extraction/Kildall.mli
OCAMLOPT extraction/FMapAVL.ml
OCAMLC   extraction/Validator_complete.mli
OCAMLOPT extraction/Interpreter.ml
OCAMLOPT extraction/Integers.ml
OCAMLOPT extraction/Binary.ml
OCAMLC   extraction/AST.mli
OCAMLC   lib/Camlcoq.ml
OCAMLOPT cparser/ErrorReports.ml
OCAMLOPT extraction/Postorder.ml
OCAMLOPT extraction/FSetAVLplus.ml
OCAMLOPT extraction/Ordered.ml
OCAMLOPT extraction/FSetAVL.ml
OCAMLC   extraction/Op.mli
OCAMLOPT extraction/Lattice.ml
OCAMLOPT extraction/Unityping.ml
OCAMLC   extraction/Values.mli
OCAMLC   extraction/Ctypes.mli
OCAMLC   common/Sections.mli
OCAMLC   backend/AisAnnot.mli
OCAMLC   extraction/Cminor.mli
OCAMLC   extraction/Events.mli
OCAMLC   debug/DebugTypes.mli
OCAMLOPT extraction/Switch.ml
OCAMLC   extraction/CSEdomain.mli
OCAMLOPT extraction/IEEE754_extra.ml
OCAMLOPT extraction/Bits.ml
OCAMLC   extraction/Machregs.mli
OCAMLOPT extraction/Registers.ml
OCAMLC   extraction/RTL.mli
OCAMLOPT extraction/Heaps.ml
OCAMLC   extraction/Memdata.mli
OCAMLC   debug/DwarfTypes.mli
OCAMLC   extraction/Asm.mli
OCAMLC   extraction/Determinism.mli
OCAMLC   extraction/Interpreter_complete.mli
OCAMLC   extraction/Unusedglob.mli
OCAMLC   extraction/CminorSel.mli
OCAMLC   extraction/Cminortyping.mli
OCAMLC   extraction/Renumber.mli
OCAMLC   extraction/ValueDomain.mli
OCAMLC   extraction/Liveness.mli
OCAMLC   extraction/Csharpminor.mli
OCAMLC   extraction/CombineOp.mli
OCAMLC   backend/Asmexpandaux.mli
OCAMLC   x86/AsmToJSON.mli
OCAMLOPT extraction/Floats.ml
OCAMLC   extraction/Locations.mli
OCAMLOPT extraction/Kildall.ml
OCAMLC   x86/Machregsaux.mli
OCAMLC   extraction/Mach.mli
OCAMLC   extraction/Memory.mli
OCAMLC   debug/Debug.mli
OCAMLOPT debug/DwarfUtil.ml
OCAMLC   debug/DwarfPrinter.mli
OCAMLC   backend/PrintAsm.mli
OCAMLC   extraction/Globalenvs.mli
OCAMLC   extraction/Builtins0.mli
OCAMLC   debug/DebugInformation.mli
OCAMLC   extraction/Linear.mli
OCAMLC   extraction/RTLgen.mli
OCAMLC   cparser/ExtendedAsm.ml
OCAMLC   extraction/ValueAOp.mli
OCAMLC   extraction/NeedDomain.mli
OCAMLC   extraction/Cminorgen.mli
OCAMLC   extraction/CleanupLabels.mli
OCAMLC   extraction/Asmgen.mli
OCAMLOPT x86/AsmToJSON.ml
OCAMLOPT lib/Camlcoq.ml
OCAMLOPT extraction/AST.ml
OCAMLC   backend/XTL.mli
OCAMLC   extraction/Conventions1.mli
OCAMLC   extraction/LTL.mli
OCAMLC   extraction/Cop.mli
OCAMLC   extraction/Builtins1.mli
OCAMLOPT extraction/Validator_complete.ml
OCAMLC   extraction/Main.mli
OCAMLC   extraction/NeedOp.mli
OCAMLC   extraction/ConstpropOp.mli
OCAMLC   extraction/Conventions.mli
OCAMLC   backend/IRC.mli
OCAMLC   extraction/Csyntax.mli
OCAMLC   extraction/Clight.mli
OCAMLC   extraction/Builtins.mli
OCAMLC   extraction/Tunneling.mli
OCAMLC   extraction/Tailcall.mli
OCAMLC   extraction/Bounds.mli
OCAMLC   extraction/Lineartyping.mli
OCAMLOPT common/Switchaux.ml
OCAMLC   extraction/SelectOp.mli
OCAMLC   extraction/Linearize.mli
OCAMLC   extraction/Debugvar.mli
OCAMLC   extraction/ValueAnalysis.mli
OCAMLC   extraction/Cshmgen.mli
OCAMLOPT driver/Timing.ml
OCAMLOPT extraction/Op.ml
OCAMLC   extraction/RTLtyping.mli
OCAMLOPT common/PrintAST.ml
OCAMLOPT extraction/Values.ml
OCAMLOPT extraction/Ctypes.ml
OCAMLOPT common/Sections.ml
OCAMLC   extraction/Initializers.mli
OCAMLC   extraction/Ctyping.mli
OCAMLOPT extraction/Cminor.ml
OCAMLOPT driver/Driveraux.ml
OCAMLOPT extraction/Events.ml
OCAMLC   extraction/Csem.mli
OCAMLOPT extraction/Interpreter_complete.ml
OCAMLC   extraction/Parser.mli
OCAMLC   driver/Frontend.mli
OCAMLC   extraction/Stacklayout.mli
OCAMLC   extraction/SimplLocals.mli
OCAMLC   extraction/SimplExpr.mli
OCAMLOPT extraction/CminorSel.ml
OCAMLC   extraction/SplitLong.mli
OCAMLOPT backend/Selectionaux.ml
OCAMLOPT extraction/Cminortyping.ml
OCAMLC   cfrontend/C2C.ml
OCAMLC   extraction/Deadcode.mli
OCAMLOPT extraction/Csharpminor.ml
OCAMLC   extraction/Constprop.mli
OCAMLOPT extraction/CSEdomain.ml
OCAMLC   extraction/CSE.mli
OCAMLC   extraction/Allocation.mli
OCAMLOPT driver/Assembler.ml
OCAMLOPT extraction/Machregs.ml
OCAMLOPT extraction/RTL.ml
OCAMLOPT x86/PrintOp.ml
OCAMLOPT extraction/Memdata.ml
OCAMLOPT debug/Debug.ml
OCAMLOPT backend/PrintCminor.ml
OCAMLOPT extraction/Asm.ml
OCAMLOPT driver/Linker.ml
OCAMLOPT extraction/Determinism.ml
OCAMLOPT extraction/Builtins0.ml
OCAMLC   extraction/Cexec.mli
OCAMLOPT cparser/Unblock.ml
OCAMLOPT extraction/Main.ml
OCAMLOPT cparser/Cleanup.ml
OCAMLOPT cparser/Bitfields.ml
OCAMLOPT debug/DebugInformation.ml
OCAMLOPT extraction/Unusedglob.ml
OCAMLC   extraction/Stacking.mli
OCAMLC   extraction/SelectLong.mli
OCAMLOPT extraction/Renumber.ml
OCAMLOPT backend/RTLgenaux.ml
OCAMLC   backend/Inliningaux.ml
OCAMLOPT extraction/ValueDomain.ml
OCAMLOPT extraction/Liveness.ml
OCAMLOPT extraction/Cminorgen.ml
OCAMLOPT extraction/CombineOp.ml
OCAMLOPT backend/Asmexpandaux.ml
OCAMLOPT extraction/Locations.ml
OCAMLOPT backend/PrintRTL.ml
OCAMLOPT extraction/Mach.ml
OCAMLOPT backend/AisAnnot.ml
OCAMLOPT extraction/Memory.ml
OCAMLOPT backend/PrintAsmaux.ml
OCAMLOPT extraction/Builtins1.ml
OCAMLOPT extraction/Parser.ml
OCAMLOPT cparser/Elab.ml
OCAMLOPT debug/Dwarfgen.ml
OCAMLOPT extraction/Linear.ml
OCAMLC   extraction/SelectDiv.mli
OCAMLOPT extraction/RTLgen.ml
OCAMLC   extraction/Inlining.mli
OCAMLOPT extraction/CleanupLabels.ml
OCAMLOPT extraction/Asmgen.ml
OCAMLOPT backend/XTL.ml
OCAMLOPT extraction/Conventions1.ml
OCAMLOPT extraction/LTL.ml
OCAMLOPT extraction/Cop.ml
OCAMLOPT debug/DwarfPrinter.ml
OCAMLOPT extraction/Builtins.ml
OCAMLOPT extraction/Globalenvs.ml
OCAMLOPT debug/DebugInit.ml
OCAMLOPT extraction/Tunneling.ml
OCAMLC   extraction/Selection.mli
OCAMLOPT backend/Linearizeaux.ml
OCAMLOPT extraction/Debugvar.ml
OCAMLOPT extraction/ValueAOp.ml
OCAMLOPT extraction/NeedDomain.ml
OCAMLC   extraction/Compiler.mli
OCAMLOPT backend/Splitting.ml
OCAMLOPT extraction/Conventions.ml
OCAMLOPT x86/Machregsaux.ml
OCAMLOPT extraction/Csyntax.ml
OCAMLOPT extraction/Clight.ml
OCAMLOPT extraction/Linearize.ml
OCAMLOPT extraction/ValueAnalysis.ml
OCAMLOPT extraction/NeedOp.ml
OCAMLOPT extraction/Cshmgen.ml
OCAMLOPT extraction/RTLtyping.ml
OCAMLOPT backend/PrintXTL.ml
OCAMLOPT backend/PrintLTL.ml
OCAMLOPT backend/PrintMach.ml
OCAMLOPT extraction/Initializers.ml
OCAMLOPT cparser/ExtendedAsm.ml
OCAMLOPT extraction/Ctyping.ml
OCAMLOPT extraction/Csem.ml
OCAMLOPT extraction/Tailcall.ml
OCAMLOPT extraction/Bounds.ml
OCAMLOPT extraction/Lineartyping.ml
OCAMLOPT extraction/SimplLocals.ml
OCAMLOPT extraction/SimplExpr.ml
OCAMLOPT extraction/Deadcode.ml
OCAMLOPT extraction/CSE.ml
OCAMLOPT x86/Asmexpand.ml
OCAMLOPT backend/IRC.ml
OCAMLOPT extraction/Cexec.ml
OCAMLOPT extraction/Stacklayout.ml
OCAMLOPT cfrontend/C2C.ml
OCAMLOPT extraction/Stacking.ml
OCAMLOPT backend/Regalloc.ml
OCAMLOPT cfrontend/PrintCsyntax.ml
OCAMLOPT x86/TargetPrinter.ml
OCAMLOPT cfrontend/CPragmas.ml
OCAMLOPT extraction/SelectOp.ml
OCAMLOPT backend/Inliningaux.ml
OCAMLOPT extraction/ConstpropOp.ml
OCAMLOPT extraction/Inlining.ml
OCAMLOPT extraction/Allocation.ml
OCAMLOPT cfrontend/PrintClight.ml
OCAMLOPT driver/Interp.ml
OCAMLOPT backend/PrintAsm.ml
OCAMLOPT extraction/SplitLong.ml
OCAMLOPT extraction/Constprop.ml
OCAMLOPT extraction/SelectLong.ml
OCAMLOPT extraction/SelectDiv.ml
OCAMLOPT extraction/Selection.ml
OCAMLOPT extraction/Compiler.ml
OCAMLOPT cparser/Lexer.ml
OCAMLOPT cparser/Parse.ml
OCAMLOPT driver/Frontend.ml
OCAMLOPT driver/Driver.ml
Linking ccomp
make[3]: Leaving directory '/Users/jcheng/vms/tools/coqup/lib/CompCert'
make[2]: Leaving directory '/Users/jcheng/vms/tools/coqup/lib/CompCert'
make runtime
make[2]: Entering directory '/Users/jcheng/vms/tools/coqup/lib/CompCert'
make -C runtime
make[3]: Entering directory '/Users/jcheng/vms/tools/coqup/lib/CompCert/runtime'
gcc -m64 -c -DMODEL_64 -DABI_standard -DENDIANNESS_little -DSYS_linux -o i64_dtou.o x86_64/i64_dtou.S
gcc -m64 -c -DMODEL_64 -DABI_standard -DENDIANNESS_little -DSYS_linux -o i64_utod.o x86_64/i64_utod.S
gcc -m64 -c -DMODEL_64 -DABI_standard -DENDIANNESS_little -DSYS_linux -o i64_utof.o x86_64/i64_utof.S
gcc -m64 -c -DMODEL_64 -DABI_standard -DENDIANNESS_little -DSYS_linux -o vararg.o x86_64/vararg.S
x86_64/i64_utod.S:41:x86_64/i64_utof.S:41:x86_64/i64_dtou.S:41:Alignment too large: 15. assumed.Alignment too large: 15. assumed.
Alignment too large: 15. assumed.

x86_64/i64_utod.S:56:Unknown pseudo-op: .typex86_64/vararg.S:65:
x86_64/i64_utof.S:56:x86_64/i64_dtou.S:55:x86_64/i64_utod.S:56:Unknown pseudo-op: .typeUnknown pseudo-op: .type
Rest of line ignored. 1st junk character valued 95 (_).Alignment too large: 15. assumed.
x86_64/i64_utof.S:56:
x86_64/i64_dtou.S:55:Rest of line ignored. 1st junk character valued 95 (_).x86_64/i64_utod.S:56:Rest of line ignored. 1st junk character valued 95 (_).

Unknown pseudo-op: .size
x86_64/i64_utof.S:56:
x86_64/i64_dtou.S:55:Unknown pseudo-op: .sizex86_64/i64_utod.S:56:Unknown pseudo-op: .size
Rest of line ignored. 1st junk character valued 95 (_).
x86_64/i64_utof.S:56:
x86_64/i64_dtou.S:55:Rest of line ignored. 1st junk character valued 95 (_).Rest of line ignored. 1st junk character valued 95 (_).

x86_64/vararg.S:81:Unknown pseudo-op: .type
x86_64/vararg.S:81:Rest of line ignored. 1st junk character valued 95 (_).
x86_64/vararg.S:81:Unknown pseudo-op: .size
x86_64/vararg.S:81:Rest of line ignored. 1st junk character valued 95 (_).
x86_64/vararg.S:83:Alignment too large: 15. assumed.
x86_64/vararg.S:99:Unknown pseudo-op: .type
x86_64/vararg.S:99:Rest of line ignored. 1st junk character valued 95 (_).
x86_64/vararg.S:99:Unknown pseudo-op: .size
x86_64/vararg.S:99:Rest of line ignored. 1st junk character valued 95 (_).
x86_64/vararg.S:101:Alignment too large: 15. assumed.
x86_64/vararg.S:117:Unknown pseudo-op: .type
x86_64/vararg.S:117:Rest of line ignored. 1st junk character valued 95 (_).
x86_64/vararg.S:117:Unknown pseudo-op: .size
x86_64/vararg.S:117:Rest of line ignored. 1st junk character valued 95 (_).
x86_64/vararg.S:119:Alignment too large: 15. assumed.
x86_64/vararg.S:121:Unknown pseudo-op: .type
x86_64/vararg.S:121:Rest of line ignored. 1st junk character valued 95 (_).
x86_64/vararg.S:121:Unknown pseudo-op: .size
x86_64/vararg.S:121:Rest of line ignored. 1st junk character valued 95 (_).
x86_64/vararg.S:130:Alignment too large: 15. assumed.
x86_64/vararg.S:148:Unknown pseudo-op: .type
x86_64/vararg.S:148:Rest of line ignored. 1st junk character valued 95 (_).
x86_64/vararg.S:148:Unknown pseudo-op: .size
x86_64/vararg.S:148:Rest of line ignored. 1st junk character valued 95 (_).
make[3]: *** [Makefile:57: i64_utof.o] Error 1
make[3]: *** Waiting for unfinished jobs....
make[3]: *** [Makefile:57: i64_utod.o] Error 1
make[3]: *** [Makefile:57: vararg.o] Error 1
make[3]: *** [Makefile:57: i64_dtou.o] Error 1
make[3]: Leaving directory '/Users/jcheng/vms/tools/coqup/lib/CompCert/runtime'
make[2]: *** [Makefile:172: runtime] Error 2
make[2]: Leaving directory '/Users/jcheng/vms/tools/coqup/lib/CompCert'
make[1]: *** [Makefile:139: all] Error 2
make[1]: Leaving directory '/Users/jcheng/vms/tools/coqup/lib/CompCert'
make: *** [Makefile:27: lib/COMPCERTSTAMP] Error 2

Optimise division implementation

Currently, the division algorithm heavily influences the frequency at which the design can run. Instead of using the division operator, it should therefore be possible to use a specialised division module, which should also be proven correct separately.

Instead, a division function in C can be used for now to go around that.

ill-formed initializer issue

Howdy,

I'm trying to generate run a 4 tap FIR filter and I'm getting the error message shown below

Would appreciate any help to find a potential solution.

command:
./bin/vericert fir_4tap.c -o fir_4tap.o

error message
fir_4tap.c:5:31: syntax error after '{' and before '}'.
Ill-formed initializer.
At this point, an optional designation, followed with an initializer, is expected.
Fatal error; compilation aborted.
1 error detected.

code
The FIR filter I'm trying to implement is described below (example taken from the Parallel Programming for FPGAs' book)

#define NUM_TAPS 4
void fir ( int input, int *output, int taps [NUM_TAPS] ) {
static int delay_line [NUM_TAPS] = {};
int result = 0;
for ( int i = NUM_TAPS -1 ; i > 0 ; i--) {
delay_line[i] = delay_line[i - 1];
}
delay_line[0] = input;
for ( int i = 0 ; i < NUM_TAPS ; i ++ ) {
result += delay_line[i] * taps[i];
}
*output = result;
}

installation issue

I just tried installing coqup (master branch, 4edb75) but hit the following error:

Johns-MacBook-Pro-3:coqup jpw48$ nix-build
these derivations will be built:
  /nix/store/rwalxr271ilygq1n06680al8jckakx32-source.drv
  /nix/store/5ygvagbvihk56d5w89w6rs23l2wqhqcf-coq8.10-bbv.drv
  /nix/store/l55gwij4yy7bw725lyvwh6awx2fgba5l-coqup.drv
these paths will be fetched (322.92 MiB download, 1581.04 MiB unpacked):
  /nix/store/009k5a1n92lrav4fh2xnz23qf2jrh7jm-patch-2.7.6
  /nix/store/08nipyxbag0vwsjs6fafvndlinm510gj-llvm-7.1.0
  /nix/store/0c288xy3i4g6c38aa067ixa5mb9lk0lf-nghttp2-1.40.0-lib
  /nix/store/0mmgv39ij03kw12znr0pkjyvawnjf4wd-zlib-1.2.11-dev
  /nix/store/12swncflm8b1nif8cfzalchki6qfdf05-stdenv-darwin
  /nix/store/1ngwf6wvh9hf1vz3h2h5znqi90fa86q1-clang-wrapper-7.1.0
  /nix/store/1q222g8p6dhjvdkhgn4vydxhx1mhbi9f-libev-4.33
  /nix/store/1xn77yix5qbxy49w734js17hyjag0vm5-unzip-6.0
  /nix/store/23fhqc2b3yqbgk2h62dnqzyhq1g8pvg8-coq-8.10.2
  /nix/store/25x2pjx54r34cklwj15mmbkc8zxk7wjn-c-ares-1.15.0
  /nix/store/2vlb0jnsz5v6w3c1q3clgzfxd47shlkz-curl-7.68.0-dev
  /nix/store/2zyg3d8hcgqn4sv7cc9k41sy49yjggdn-curl-7.68.0-man
  /nix/store/3anjymbdrfcf5sqyq3zdmb5mnkrfnv3v-nghttp2-1.40.0-dev
  /nix/store/3b5092bc3xa5gxwr4sxkvh3b9d4iypz2-clang-7.1.0-lib
  /nix/store/47m4h1bb5df8k6031qbljfr4w3m63f68-libc++-7.1.0
  /nix/store/4fxk0lf2zy3ib7488fh7573naa53jq37-xz-5.2.5
  /nix/store/4m1zvi1rmjf32rwqqmwsa4v181nfvycb-expand-response-params
  /nix/store/4p3bds5cknzwg72np1rzyn3jq0962z84-bash-4.4-p23
  /nix/store/4q0y4pbgc82lj7llxwj5n6ly2xsc5hm7-openssl-1.1.1d-dev
  /nix/store/6wf9n219synck5gbkrk0zrb9qg4bgz3c-bzip2-1.0.6.0.1-bin
  /nix/store/7955xrl5hg078v0ip0ki8wnm7kqx44kl-ncurses-6.2-dev
  /nix/store/7j9543gj0idrcimyxg9rkfdnkcgav3bp-gettext-0.20.1
  /nix/store/7x9a14vrl2mfrg89nhik3vq8z086lq1y-gfortran-9.3.0-lib
  /nix/store/7y6vn8wr00zwkcnv830qjkra37gvd11p-gettext-0.20.1
  /nix/store/7zryalm91s9im117zvq1hcgzs42al0g7-libiconv-osx-10.12.6
  /nix/store/81rb87agmp9cbsvg2xm2n4kp9c6309lv-ncurses-6.2
  /nix/store/87bk6piv948k764i0cin48vhv9s1ymn9-nghttp2-1.40.0-bin
  /nix/store/88z08d33mc8ymkxv006zp43lagdr327j-ocaml-4.09.1
  /nix/store/8r83yw77k1cbpcbvvwiwxi047rgiba6r-gcc-wrapper-9.3.0
  /nix/store/8z9kzsdjyncfq51whxlihbnkz8f16vy5-bzip2-1.0.6.0.1
  /nix/store/951rfqjj70an91lwzz7lwz67rg8yzxfz-menhir-20190626
  /nix/store/9bvvaa06570pib2c9p8m2rjb47fsrfs5-libffi-3.3
  /nix/store/9in7vl1f3dyis8k3kyc6qc9vsgg8735m-stdenv-darwin
  /nix/store/a79h3hc5izpxkrpafc1g4kkzb22yl7is-zlib-1.2.11
  /nix/store/a8dl27c6phbd9g2ml7yycyljn00v3x97-xz-5.2.5-bin
  /nix/store/ayn43f7la4dacipvbd2r9q373bspv3y5-openssl-1.1.1d-bin
  /nix/store/bak7c725z70hwwfjx14zvgxyd109zz41-expand-response-params
  /nix/store/c19aq0fh668s6q5pha75my8wmndpzfxf-dune-1.11.4
  /nix/store/d66n620h6mzdsrwksjs1ik7w3s42107b-libssh2-1.9.0
  /nix/store/f9rirp60zkzin9cxp4a4d2c3pvw8n027-compiler-rt-7.1.0
  /nix/store/fb1cjkwb8bha530wabxxqn32xzijgjw8-gmp-6.2.0
  /nix/store/fxplyfw6p0xrp61m6mhaxxil2br00kfp-llvm-7.1.0-lib
  /nix/store/gc46vimya56ss3lncapw7sdn5z0162l3-curl-7.68.0
  /nix/store/gnqq3wkfcbcryjmwkaxndw2g4xgamygv-binutils-2.31.1
  /nix/store/gw3ygl9rya28a74jv99bky9xzg04h0hx-gawk-5.0.1
  /nix/store/hgb8ykjhfk05fiwshz5ial6v83j0ssqb-ocaml-findlib-1.8.1
  /nix/store/hj85vcq46xk7x3ijk2w4x3kbjl6r7xa1-gcc-9.3.0-lib
  /nix/store/hz71p4lbzhn90vi9yacxyw42b5baiyl2-coreutils-8.31
  /nix/store/i5p6snm3s4wmmbif4fkjjaqlaycj8fm5-Libsystem-osx-10.12.6
  /nix/store/iv6rwmig8275lhds5n62k3w9cqwv3fpj-nghttp2-1.40.0-lib
  /nix/store/j53wgkqy59pih1w8pz44hskhrivnz3jh-libkrb5-1.18
  /nix/store/jhzqb2ar196ah8ar8wa3l703x15jbbsd-libssh2-1.9.0-dev
  /nix/store/jlhva5dy674rm4w91bbnyip2p6ij7wa1-swift-corefoundation
  /nix/store/jnkg82sd6kv22iaccgq79h86wdpryja5-gnutar-1.32
  /nix/store/jsspspmr3cm0b9w7gc365d2ppq8kk7x1-compiler-rt-7.1.0-dev
  /nix/store/jswqkbfhaf27nwbch4x6afmba40j46l5-openssl-1.1.1d
  /nix/store/nccijbipzpw4y6jkyr6h22jjwqhhnh6r-mpfr-4.0.2
  /nix/store/nfb90w47wml828m8bycykhd7gfbql3if-nghttp2-1.40.0
  /nix/store/nqsqc671iw4ngzlf1s40s7iy9vf5flk7-gzip-1.10
  /nix/store/p26faqrnlkwynjdrgl5ng6j4a3s1h1rk-pcre-8.44
  /nix/store/pg5q1mhsfmbk9sn5yagvzbd0dfhr737k-curl-7.68.0
  /nix/store/pk869gvnslszr8f0k9k1209pgfd8mpm3-libmpc-1.1.0
  /nix/store/q6vcxyrr0anr6hc8hwvx7jjbp7ci0z3k-ICU-osx-10.10.5
  /nix/store/qj4y7q0pb9cc9wjwk4dmvbx53d2kwpq4-gnumake-4.2.1
  /nix/store/qjfcs4kbq33qndybdizpp7xrsdx43px9-libxml2-2.9.10
  /nix/store/r5nwlqrwqkpx85hhf1q5j1jkgfvmk7gc-diffutils-3.7
  /nix/store/r8136nw2x3s2yhrbiq5p26lz62xrj5j3-cctools-port
  /nix/store/rxmf15h0n4gglfiza4rxqif49rv25nzc-libc++abi-7.1.0
  /nix/store/s0zdf9c8v3421b4qndp5npfbzf4h4pll-camlp5-7.11
  /nix/store/s2gpzzixrm9xmzym2py4w1zln4dr2hgh-gcc-9.3.0
  /nix/store/v1pa6217x3yi6gms06y6xqnc48dayqb4-gnused-4.8
  /nix/store/v8561qp6ifmblkc8q2xsig9dl8c3sfj4-adv_cmds-osx-10.5.8-locale
  /nix/store/vbv17cmdp71q6n9lvy1bwlf23ccb4va9-mirrors-list
  /nix/store/vs07zwi9mnqrcrinrggfb5n465i8y6wp-libssh2-1.9.0
  /nix/store/w03sx2iyra2is64ybjn6ps1kw2gaqvw0-cctools-binutils-darwin-927.0.2
  /nix/store/w4p33hisv8rxig7b506806j5djdk5lkn-openssl-1.1.1d
  /nix/store/w4vj07i9cq1g9vg9y0l44ijy80k9hlwz-findutils-4.7.0
  /nix/store/w78a567dc5phiy7f1xvyim62d6wlydal-cctools-binutils-darwin-wrapper-927.0.2
  /nix/store/w7sfzkp1j8vxby846jls0m560hj7rmmg-blas-3.8.0
  /nix/store/x9mz63vfknb076bqv06simqsb003vq32-curl-7.68.0-bin
  /nix/store/xbd074qa4p62sjbcmkvbzrb1d4zcj79n-clang-7.1.0
  /nix/store/xqn9fppqna4p71lwjnndq6bsv3pb7h5q-csdp-6.1.1
  /nix/store/ych43swl3x9p4brm27kpchpqa8jpal4x-ed-1.16
  /nix/store/z3d9cpkfr8y9j44jarmw56i193f6j27j-ncurses-6.2-man
  /nix/store/zak500ybyjk4yiqm6yxcxs418jpi80v4-gnugrep-3.4
copying path '/nix/store/i5p6snm3s4wmmbif4fkjjaqlaycj8fm5-Libsystem-osx-10.12.6' from 'https://cache.nixos.org'...
copying path '/nix/store/v8561qp6ifmblkc8q2xsig9dl8c3sfj4-adv_cmds-osx-10.5.8-locale' from 'https://cache.nixos.org'...
copying path '/nix/store/4p3bds5cknzwg72np1rzyn3jq0962z84-bash-4.4-p23' from 'https://cache.nixos.org'...
copying path '/nix/store/8z9kzsdjyncfq51whxlihbnkz8f16vy5-bzip2-1.0.6.0.1' from 'https://cache.nixos.org'...
copying path '/nix/store/2zyg3d8hcgqn4sv7cc9k41sy49yjggdn-curl-7.68.0-man' from 'https://cache.nixos.org'...
copying path '/nix/store/6wf9n219synck5gbkrk0zrb9qg4bgz3c-bzip2-1.0.6.0.1-bin' from 'https://cache.nixos.org'...
copying path '/nix/store/ych43swl3x9p4brm27kpchpqa8jpal4x-ed-1.16' from 'https://cache.nixos.org'...
copying path '/nix/store/4m1zvi1rmjf32rwqqmwsa4v181nfvycb-expand-response-params' from 'https://cache.nixos.org'...
copying path '/nix/store/gw3ygl9rya28a74jv99bky9xzg04h0hx-gawk-5.0.1' from 'https://cache.nixos.org'...
copying path '/nix/store/qj4y7q0pb9cc9wjwk4dmvbx53d2kwpq4-gnumake-4.2.1' from 'https://cache.nixos.org'...
copying path '/nix/store/v1pa6217x3yi6gms06y6xqnc48dayqb4-gnused-4.8' from 'https://cache.nixos.org'...
copying path '/nix/store/nqsqc671iw4ngzlf1s40s7iy9vf5flk7-gzip-1.10' from 'https://cache.nixos.org'...
copying path '/nix/store/rxmf15h0n4gglfiza4rxqif49rv25nzc-libc++abi-7.1.0' from 'https://cache.nixos.org'...
copying path '/nix/store/9bvvaa06570pib2c9p8m2rjb47fsrfs5-libffi-3.3' from 'https://cache.nixos.org'...
copying path '/nix/store/47m4h1bb5df8k6031qbljfr4w3m63f68-libc++-7.1.0' from 'https://cache.nixos.org'...
copying path '/nix/store/7zryalm91s9im117zvq1hcgzs42al0g7-libiconv-osx-10.12.6' from 'https://cache.nixos.org'...
copying path '/nix/store/q6vcxyrr0anr6hc8hwvx7jjbp7ci0z3k-ICU-osx-10.10.5' from 'https://cache.nixos.org'...
copying path '/nix/store/r8136nw2x3s2yhrbiq5p26lz62xrj5j3-cctools-port' from 'https://cache.nixos.org'...
copying path '/nix/store/f9rirp60zkzin9cxp4a4d2c3pvw8n027-compiler-rt-7.1.0' from 'https://cache.nixos.org'...
copying path '/nix/store/7j9543gj0idrcimyxg9rkfdnkcgav3bp-gettext-0.20.1' from 'https://cache.nixos.org'...
copying path '/nix/store/jsspspmr3cm0b9w7gc365d2ppq8kk7x1-compiler-rt-7.1.0-dev' from 'https://cache.nixos.org'...
copying path '/nix/store/fb1cjkwb8bha530wabxxqn32xzijgjw8-gmp-6.2.0' from 'https://cache.nixos.org'...
copying path '/nix/store/jnkg82sd6kv22iaccgq79h86wdpryja5-gnutar-1.32' from 'https://cache.nixos.org'...
copying path '/nix/store/hz71p4lbzhn90vi9yacxyw42b5baiyl2-coreutils-8.31' from 'https://cache.nixos.org'...
copying path '/nix/store/j53wgkqy59pih1w8pz44hskhrivnz3jh-libkrb5-1.18' from 'https://cache.nixos.org'...
copying path '/nix/store/r5nwlqrwqkpx85hhf1q5j1jkgfvmk7gc-diffutils-3.7' from 'https://cache.nixos.org'...
copying path '/nix/store/w4vj07i9cq1g9vg9y0l44ijy80k9hlwz-findutils-4.7.0' from 'https://cache.nixos.org'...
copying path '/nix/store/vbv17cmdp71q6n9lvy1bwlf23ccb4va9-mirrors-list' from 'https://cache.nixos.org'...
copying path '/nix/store/81rb87agmp9cbsvg2xm2n4kp9c6309lv-ncurses-6.2' from 'https://cache.nixos.org'...
copying path '/nix/store/z3d9cpkfr8y9j44jarmw56i193f6j27j-ncurses-6.2-man' from 'https://cache.nixos.org'...
copying path '/nix/store/nfb90w47wml828m8bycykhd7gfbql3if-nghttp2-1.40.0' from 'https://cache.nixos.org'...
copying path '/nix/store/7955xrl5hg078v0ip0ki8wnm7kqx44kl-ncurses-6.2-dev' from 'https://cache.nixos.org'...
copying path '/nix/store/0c288xy3i4g6c38aa067ixa5mb9lk0lf-nghttp2-1.40.0-lib' from 'https://cache.nixos.org'...
copying path '/nix/store/jswqkbfhaf27nwbch4x6afmba40j46l5-openssl-1.1.1d' from 'https://cache.nixos.org'...
copying path '/nix/store/009k5a1n92lrav4fh2xnz23qf2jrh7jm-patch-2.7.6' from 'https://cache.nixos.org'...
copying path '/nix/store/p26faqrnlkwynjdrgl5ng6j4a3s1h1rk-pcre-8.44' from 'https://cache.nixos.org'...
copying path '/nix/store/4fxk0lf2zy3ib7488fh7573naa53jq37-xz-5.2.5' from 'https://cache.nixos.org'...
copying path '/nix/store/zak500ybyjk4yiqm6yxcxs418jpi80v4-gnugrep-3.4' from 'https://cache.nixos.org'...
copying path '/nix/store/a8dl27c6phbd9g2ml7yycyljn00v3x97-xz-5.2.5-bin' from 'https://cache.nixos.org'...
copying path '/nix/store/a79h3hc5izpxkrpafc1g4kkzb22yl7is-zlib-1.2.11' from 'https://cache.nixos.org'...
copying path '/nix/store/gnqq3wkfcbcryjmwkaxndw2g4xgamygv-binutils-2.31.1' from 'https://cache.nixos.org'...
copying path '/nix/store/vs07zwi9mnqrcrinrggfb5n465i8y6wp-libssh2-1.9.0' from 'https://cache.nixos.org'...
copying path '/nix/store/qjfcs4kbq33qndybdizpp7xrsdx43px9-libxml2-2.9.10' from 'https://cache.nixos.org'...
copying path '/nix/store/gc46vimya56ss3lncapw7sdn5z0162l3-curl-7.68.0' from 'https://cache.nixos.org'...
copying path '/nix/store/fxplyfw6p0xrp61m6mhaxxil2br00kfp-llvm-7.1.0-lib' from 'https://cache.nixos.org'...
copying path '/nix/store/jlhva5dy674rm4w91bbnyip2p6ij7wa1-swift-corefoundation' from 'https://cache.nixos.org'...
copying path '/nix/store/3b5092bc3xa5gxwr4sxkvh3b9d4iypz2-clang-7.1.0-lib' from 'https://cache.nixos.org'...
copying path '/nix/store/25x2pjx54r34cklwj15mmbkc8zxk7wjn-c-ares-1.15.0' from 'https://cache.nixos.org'...
copying path '/nix/store/xbd074qa4p62sjbcmkvbzrb1d4zcj79n-clang-7.1.0' from 'https://cache.nixos.org'...
copying path '/nix/store/bak7c725z70hwwfjx14zvgxyd109zz41-expand-response-params' from 'https://cache.nixos.org'...
copying path '/nix/store/7y6vn8wr00zwkcnv830qjkra37gvd11p-gettext-0.20.1' from 'https://cache.nixos.org'...
copying path '/nix/store/1q222g8p6dhjvdkhgn4vydxhx1mhbi9f-libev-4.33' from 'https://cache.nixos.org'...
copying path '/nix/store/hj85vcq46xk7x3ijk2w4x3kbjl6r7xa1-gcc-9.3.0-lib' from 'https://cache.nixos.org'...
copying path '/nix/store/7x9a14vrl2mfrg89nhik3vq8z086lq1y-gfortran-9.3.0-lib' from 'https://cache.nixos.org'...
copying path '/nix/store/nccijbipzpw4y6jkyr6h22jjwqhhnh6r-mpfr-4.0.2' from 'https://cache.nixos.org'...
copying path '/nix/store/w7sfzkp1j8vxby846jls0m560hj7rmmg-blas-3.8.0' from 'https://cache.nixos.org'...
copying path '/nix/store/pk869gvnslszr8f0k9k1209pgfd8mpm3-libmpc-1.1.0' from 'https://cache.nixos.org'...
copying path '/nix/store/xqn9fppqna4p71lwjnndq6bsv3pb7h5q-csdp-6.1.1' from 'https://cache.nixos.org'...
copying path '/nix/store/s2gpzzixrm9xmzym2py4w1zln4dr2hgh-gcc-9.3.0' from 'https://cache.nixos.org'...
copying path '/nix/store/iv6rwmig8275lhds5n62k3w9cqwv3fpj-nghttp2-1.40.0-lib' from 'https://cache.nixos.org'...
copying path '/nix/store/88z08d33mc8ymkxv006zp43lagdr327j-ocaml-4.09.1' from 'https://cache.nixos.org'...
copying path '/nix/store/w4p33hisv8rxig7b506806j5djdk5lkn-openssl-1.1.1d' from 'https://cache.nixos.org'...
copying path '/nix/store/s0zdf9c8v3421b4qndp5npfbzf4h4pll-camlp5-7.11' from 'https://cache.nixos.org'...
copying path '/nix/store/c19aq0fh668s6q5pha75my8wmndpzfxf-dune-1.11.4' from 'https://cache.nixos.org'...
copying path '/nix/store/d66n620h6mzdsrwksjs1ik7w3s42107b-libssh2-1.9.0' from 'https://cache.nixos.org'...
copying path '/nix/store/951rfqjj70an91lwzz7lwz67rg8yzxfz-menhir-20190626' from 'https://cache.nixos.org'...
copying path '/nix/store/pg5q1mhsfmbk9sn5yagvzbd0dfhr737k-curl-7.68.0' from 'https://cache.nixos.org'...
copying path '/nix/store/jhzqb2ar196ah8ar8wa3l703x15jbbsd-libssh2-1.9.0-dev' from 'https://cache.nixos.org'...
copying path '/nix/store/x9mz63vfknb076bqv06simqsb003vq32-curl-7.68.0-bin' from 'https://cache.nixos.org'...
copying path '/nix/store/87bk6piv948k764i0cin48vhv9s1ymn9-nghttp2-1.40.0-bin' from 'https://cache.nixos.org'...
copying path '/nix/store/hgb8ykjhfk05fiwshz5ial6v83j0ssqb-ocaml-findlib-1.8.1' from 'https://cache.nixos.org'...
copying path '/nix/store/3anjymbdrfcf5sqyq3zdmb5mnkrfnv3v-nghttp2-1.40.0-dev' from 'https://cache.nixos.org'...
copying path '/nix/store/23fhqc2b3yqbgk2h62dnqzyhq1g8pvg8-coq-8.10.2' from 'https://cache.nixos.org'...
copying path '/nix/store/ayn43f7la4dacipvbd2r9q373bspv3y5-openssl-1.1.1d-bin' from 'https://cache.nixos.org'...
copying path '/nix/store/9in7vl1f3dyis8k3kyc6qc9vsgg8735m-stdenv-darwin' from 'https://cache.nixos.org'...
copying path '/nix/store/4q0y4pbgc82lj7llxwj5n6ly2xsc5hm7-openssl-1.1.1d-dev' from 'https://cache.nixos.org'...
copying path '/nix/store/1xn77yix5qbxy49w734js17hyjag0vm5-unzip-6.0' from 'https://cache.nixos.org'...
copying path '/nix/store/0mmgv39ij03kw12znr0pkjyvawnjf4wd-zlib-1.2.11-dev' from 'https://cache.nixos.org'...
copying path '/nix/store/2vlb0jnsz5v6w3c1q3clgzfxd47shlkz-curl-7.68.0-dev' from 'https://cache.nixos.org'...
copying path '/nix/store/08nipyxbag0vwsjs6fafvndlinm510gj-llvm-7.1.0' from 'https://cache.nixos.org'...
building '/nix/store/rwalxr271ilygq1n06680al8jckakx32-source.drv'...

trying https://github.com/mit-plv/bbv/archive/5099237c52d2910f79a1a3ca9ae4dfa80129bf86.tar.gz
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
100   153  100   153    0     0    993      0 --:--:-- --:--:-- --:--:--   993
100 51982    0 51982    0     0  71997      0 --:--:-- --:--:-- --:--:--  135k
unpacking source archive /private/var/folders/js/z_kj2f215t9844dczy96r_hr0000gn/T/nix-build-source.drv-0/5099237c52d2910f79a1a3ca9ae4dfa80129bf86.tar.gz
copying path '/nix/store/w03sx2iyra2is64ybjn6ps1kw2gaqvw0-cctools-binutils-darwin-927.0.2' from 'https://cache.nixos.org'...
copying path '/nix/store/w78a567dc5phiy7f1xvyim62d6wlydal-cctools-binutils-darwin-wrapper-927.0.2' from 'https://cache.nixos.org'...
copying path '/nix/store/1ngwf6wvh9hf1vz3h2h5znqi90fa86q1-clang-wrapper-7.1.0' from 'https://cache.nixos.org'...
copying path '/nix/store/8r83yw77k1cbpcbvvwiwxi047rgiba6r-gcc-wrapper-9.3.0' from 'https://cache.nixos.org'...
copying path '/nix/store/12swncflm8b1nif8cfzalchki6qfdf05-stdenv-darwin' from 'https://cache.nixos.org'...
building '/nix/store/5ygvagbvihk56d5w89w6rs23l2wqhqcf-coq8.10-bbv.drv'...
unpacking sources
unpacking source archive /nix/store/98phrsgw9p8qhwp30ch81r6bqmjnhx6v-source
source root is source
patching sources
configuring
no configure script, doing nothing
building
build flags: -j4 -l4 SHELL=/nix/store/4p3bds5cknzwg72np1rzyn3jq0962z84-bash-4.4-p23/bin/bash
coq_makefile -f _CoqProject ./src/bbv/NLib.v ./src/bbv/DepEq.v ./src/bbv/BinNotationZ.v ./src/bbv/Nomega.v ./src/bbv/NatLib.v ./src/bbv/ZLib.v ./src/bbv/DepEqNat.v ./src/bbv/ReservedNotations.v ./src/bbv/HexNotation.v ./src/bbv/BinNotation.v ./src/bbv/HexNotationZ.v ./src/bbv/WordScope.v ./src/bbv/ZHints.v ./src/bbv/Word.v ./src/bbv/HexNotationWord.v ./src/bbv/N_Z_nat_conversions.v -o Makefile.coq.all
make -f Makefile.coq.all
make[1]: Entering directory '/private/var/folders/js/z_kj2f215t9844dczy96r_hr0000gn/T/nix-build-coq8.10-bbv.drv-0/source'
COQDEP VFILES
COQC src/bbv/NLib.v
COQC src/bbv/ReservedNotations.v
COQC src/bbv/Nomega.v
COQC src/bbv/N_Z_nat_conversions.v
COQC src/bbv/ZLib.v
COQC src/bbv/DepEqNat.v
COQC src/bbv/HexNotation.v
COQC src/bbv/ZHints.v
COQC src/bbv/NatLib.v
COQC src/bbv/HexNotationZ.v
COQC src/bbv/BinNotation.v
COQC src/bbv/DepEq.v
COQC src/bbv/BinNotationZ.v
COQC src/bbv/Word.v
File "./src/bbv/Word.v", line 27, characters 0-35:
Warning: Declaring a scope implicitly is deprecated; use in advance an
explicit "Declare Scope word_scope.". [undeclared-scope,deprecated]
File "./src/bbv/Word.v", line 155, characters 0-28:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
File "./src/bbv/Word.v", line 446, characters 0-45:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
File "./src/bbv/Word.v", line 1136, characters 0-43:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
File "./src/bbv/Word.v", line 1268, characters 0-42:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
File "./src/bbv/Word.v", line 2265, characters 0-28:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
COQC src/bbv/WordScope.v
COQC src/bbv/HexNotationWord.v
make[1]: Leaving directory '/private/var/folders/js/z_kj2f215t9844dczy96r_hr0000gn/T/nix-build-coq8.10-bbv.drv-0/source'
installing
INSTALL ./src/bbv/NLib.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/DepEq.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/BinNotationZ.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/Nomega.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/NatLib.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/ZLib.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/DepEqNat.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/ReservedNotations.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/HexNotation.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/BinNotation.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/HexNotationZ.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/WordScope.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/ZHints.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/Word.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/HexNotationWord.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/N_Z_nat_conversions.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/NLib.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/DepEq.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/BinNotationZ.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/Nomega.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/NatLib.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/ZLib.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/DepEqNat.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/ReservedNotations.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/HexNotation.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/BinNotation.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/HexNotationZ.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/WordScope.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/ZHints.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/Word.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/HexNotationWord.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/N_Z_nat_conversions.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/NLib.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/DepEq.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/BinNotationZ.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/Nomega.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/NatLib.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/ZLib.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/DepEqNat.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/ReservedNotations.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/HexNotation.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/BinNotation.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/HexNotationZ.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/WordScope.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/ZHints.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/Word.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/HexNotationWord.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/N_Z_nat_conversions.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
make[1]: Entering directory '/private/var/folders/js/z_kj2f215t9844dczy96r_hr0000gn/T/nix-build-coq8.10-bbv.drv-0/source'
make[1]: Leaving directory '/private/var/folders/js/z_kj2f215t9844dczy96r_hr0000gn/T/nix-build-coq8.10-bbv.drv-0/source'
post-installation fixup
strip is /nix/store/w03sx2iyra2is64ybjn6ps1kw2gaqvw0-cctools-binutils-darwin-927.0.2/bin/strip
stripping (with command strip and flags -S) in /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib 
patching script interpreter paths in /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv
building '/nix/store/l55gwij4yy7bw725lyvwh6awx2fgba5l-coqup.drv'...
unpacking sources
unpacking source archive /nix/store/mplhq2zjqgmag56sl09j7c0az37czg4s-coqup
source root is coqup
patching sources
configuring
no configure script, doing nothing
building
build flags: -j4 -l4 SHELL=/nix/store/4p3bds5cknzwg72np1rzyn3jq0962z84-bash-4.4-p23/bin/bash
(cd lib/CompCert && ./configure x86_64-linux)
/nix/store/4p3bds5cknzwg72np1rzyn3jq0962z84-bash-4.4-p23/bin/bash: ./configure: No such file or directory
make: *** [Makefile:26: lib/COMPCERTSTAMP] Error 127
builder for '/nix/store/l55gwij4yy7bw725lyvwh6awx2fgba5l-coqup.drv' failed with exit code 2
error: build of '/nix/store/l55gwij4yy7bw725lyvwh6awx2fgba5l-coqup.drv' failed

Compile failed.

I just gave it a first go, and the tool reports no main.c file so I created a new one:

int main(){
  int k, i;
  for (i = 0; i < 10; i++)
    k += i;
  return k;
}

Then I got this:

[nix-shell:/tools/coqup]$ ./bin/coqup main.c -o main.v
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:1:no such instruction: `module main(reg_6, reg_7,reg_8,reg_4,reg_5)'
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:2:no such instruction: `input [0:0] reg_6'
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:3:no such instruction: `input [0:0] reg_7'
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:4:no such instruction: `input [0:0] reg_8'
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:5:no such instruction: `output reg [0:0] reg_4'
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:6:no such instruction: `output reg [31:0] reg_5'
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:7:no such instruction: `always @(posedge reg_8 or posedge reg_7)'
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:8:no such instruction: `if ((reg_7 ==1(100)1))'
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:9:invalid character '_' in mnemonic
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:10:no such instruction: `else'
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:11:no such instruction: `case (reg_9)'
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:12:Junk character 52 (4).
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:12:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:13:invalid character '_' in mnemonic
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:14:Junk character 51 (3).
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:14:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:15:invalid character '_' in mnemonic
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:16:Junk character 50 (2).
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:16:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:17:invalid character '_' in mnemonic
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:18:Junk character 51 (3).
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:18:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:19:invalid character '_' in mnemonic
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:20:Junk character 49 (1).
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:20:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:21:invalid character '_' in mnemonic
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:22:Junk character 52 (4).
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:22:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:23:invalid character '_' in mnemonic
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:24:Junk character 51 (3).
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:24:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:25:invalid character '_' in mnemonic
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:26:Junk character 50 (2).
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:26:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:27:invalid character '_' in mnemonic
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:28:Junk character 51 (3).
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:28:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:29:invalid character '_' in mnemonic
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:31:no such instruction: `endcase'
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:32:no such instruction: `always @*'
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:33:no such instruction: `case (reg_9)'
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:34:Junk character 52 (4).
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:34:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:36:Junk character 51 (3).
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:36:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:38:Junk character 50 (2).
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:38:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:39:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:40:Junk character 51 (3).
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:40:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:41:Missing ')' assumed
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:41:Can't relocate expression. Absolute 0 assumed.
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:41:Missing ')' assumed
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:41:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:42:Junk character 49 (1).
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:42:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:43:no such instruction: `begin'
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:44:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:46:no such instruction: `end'
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:47:Junk character 52 (4).
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:47:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:48:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:49:Junk character 51 (3).
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:49:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:50:Missing ')' assumed
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:50:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:51:Junk character 50 (2).
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:51:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:53:Junk character 51 (3).
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:53:Rest of line ignored. 1st junk character valued 40 (().
/var/folders/vf/cnx53rv902z35wzp5qqxthgr0000gn/T/compcertd91a7d.s:55:FATAL:Symbol default already defined.
ccomp: error: assembler command failed with exit code 1 (use -v to see invocation)

Then I found there is an existing main.c in the examples folder. I try to run it but it got the same error...

Implement Oshrximm

Currently Oshrximm is not implemented, as it needs to be implemented with a division.

One reason for the mismatch between division and shift is shown below:

-11 / (1 << 1) = -5
-11 >>> 1      = -6

Therefore it will always be more efficient to use unsigned division by a constant compared to signed division by a constant.

Maybe there is a more efficient implementation of this special case.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.