Collapse file tree

Files

 master

Search this repository

/

backend

/

Copy path

Directory actions

More options

More options

Directory actions

More options

More options

Latest commit

xavierleroy

Add From Coq to Require of standard library modules

Open commit details

May 5, 2025

5e4ef44 · May 5, 2025

History

History

Open commit details

/

backend

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
AisAnnot.ml		AisAnnot.ml	Add newline directly on list in annot.	Mar 13, 2018
AisAnnot.mli		AisAnnot.mli	Print symbols as symbols.	Mar 8, 2018
Allocation.v		Allocation.v	Add From Coq to Require of standard library modules	May 5, 2025
Allocproof.v		Allocproof.v	Add From Coq to Require of standard library modules	May 5, 2025
Asmexpandaux.ml		Asmexpandaux.ml	Replace AST.rettype by AST.xtype	Jul 15, 2024
Asmexpandaux.mli		Asmexpandaux.mli	Fix misspellings in messages, man pages, and comments	May 31, 2019
Asmgenproof0.v		Asmgenproof0.v	Qualify Hint as Global Hint where appropriate	Jan 21, 2021
Bounds.v		Bounds.v	Add From Coq to Require of standard library modules	May 5, 2025
CSE.v		CSE.v	Less aggressive CSE across calls to known runtime functions	Mar 21, 2025
CSEdomain.v		CSEdomain.v	CSE for known builtin functions	Mar 21, 2025
CSEproof.v		CSEproof.v	Less aggressive CSE across calls to known runtime functions	Mar 21, 2025
CleanupLabels.v		CleanupLabels.v	Add From Coq to Require of standard library modules	May 5, 2025
CleanupLabelsproof.v		CleanupLabelsproof.v	Add From Coq to Require of standard library modules	May 5, 2025
Cminor.v		Cminor.v	Enforce well-typedness of function parameters from C#minor to RTL	Jul 15, 2024
CminorSel.v		CminorSel.v	Binding a list of CminorSel expressions to let-variables	Apr 25, 2025
Cminortyping.v		Cminortyping.v	Replace AST.rettype by AST.xtype	Jul 15, 2024
Constprop.v		Constprop.v	Perform constant propagation for known built-in functions	Jul 17, 2019
Constpropproof.v		Constpropproof.v	Enforce well-typedness of function parameters from C#minor to RTL	Jul 15, 2024
Conventions.v		Conventions.v	Replace omega tactic with lia	Dec 29, 2020
Deadcode.v		Deadcode.v	Dead code elimination for calls to known runtime functions	Mar 21, 2025
Deadcodeproof.v		Deadcodeproof.v	Add From Coq to Require of standard library modules	May 5, 2025
Debugvar.v		Debugvar.v	Transform non-recursive Fixpoint into Definition	Jun 21, 2020
Debugvarproof.v		Debugvarproof.v	Remove coq warnings (#28)	Sep 22, 2017
Fileinfo.ml		Fileinfo.ml	Ensure that there are file directives for all files used in the debug	Oct 4, 2015
IRC.ml		IRC.ml	Change preference for new register in allocator	Mar 6, 2023
IRC.mli		IRC.mli	Move reserved_registers to CPragmas.	Apr 20, 2020
Inlining.v		Inlining.v	Use name instead of ident in notations for monads	Nov 27, 2024
Inliningaux.ml		Inliningaux.ml	Cosmetic: in OCaml code, write "open! Module" instead of "open !Module"	Feb 21, 2020
Inliningaux.mli		Inliningaux.mli	Add explicit interface for backend/Inliningaux	May 5, 2025
Inliningproof.v		Inliningproof.v	Enforce well-typedness of function parameters from C#minor to RTL	Jul 15, 2024
Inliningspec.v		Inliningspec.v	Replace omega tactic with lia	Dec 29, 2020
Json.ml		Json.ml	Reworked json export.	Sep 12, 2019
JsonAST.ml		JsonAST.ml	Support mergeable sections for fixed-size literals	Aug 29, 2022
JsonAST.mli		JsonAST.mli	Reworked json export.	Sep 12, 2019
Kildall.v		Kildall.v	Remove coq warnings (#28)	Sep 22, 2017
LTL.v		LTL.v	Treat Outgoing stack slots as caller-save in LTL/Linear semantics (#237)	Jun 17, 2018
Linear.v		Linear.v	Model external calls as destroying all caller-save registers	Jun 1, 2018
Linearize.v		Linearize.v	Add From Coq to Require of standard library modules	May 5, 2025
Linearizeaux.ml		Linearizeaux.ml	Compatibility with OCaml 4.08 (#302)	Jul 8, 2019
Linearizeproof.v		Linearizeproof.v	Add From Coq to Require of standard library modules	May 5, 2025
Lineartyping.v		Lineartyping.v	Improved auto goal selection (#443)	Sep 8, 2022
Liveness.v		Liveness.v	Updated PR by removing whitespaces. Bug 17450.	Oct 20, 2015
Locations.v		Locations.v	Add From Coq to Require of standard library modules	May 5, 2025
Mach.v		Mach.v	Model external calls as destroying all caller-save registers	Jun 1, 2018
Machregsnames.ml		Machregsnames.ml	Move shared code in new file.	Jun 28, 2020
Machregsnames.mli		Machregsnames.mli	Move shared code in new file.	Jun 28, 2020
NeedDomain.v		NeedDomain.v	NeedDomain: add abstract operators for 32-bit / 64-bit integer conver…	Feb 4, 2025
PrintAsm.ml		PrintAsm.ml	Mark stack as non-executable in binaries produced by ccomp	Sep 2, 2024
PrintAsm.mli		PrintAsm.mli	Code cleanup.	Mar 10, 2016
PrintAsmaux.ml		PrintAsmaux.ml	Mark stack as non-executable in binaries produced by ccomp	Sep 2, 2024
PrintCminor.ml		PrintCminor.ml	Replace AST.rettype by AST.xtype	Jul 15, 2024
PrintLTL.ml		PrintLTL.ml	Move shared code in new file.	Jun 28, 2020
PrintMach.ml		PrintMach.ml	Move shared code in new file.	Jun 28, 2020
PrintRTL.ml		PrintRTL.ml	Compatibility with OCaml 4.08 (#302)	Jul 8, 2019
PrintXTL.ml		PrintXTL.ml	Move shared code in new file.	Jun 28, 2020
RTL.v		RTL.v	Refactoring: move is_known_runtime_function to RTL	Mar 21, 2025
RTLgen.v		RTLgen.v	Use name instead of ident in notations for monads	Nov 27, 2024
RTLgenaux.ml		RTLgenaux.ml	Bound the recursion depth of size_stmt (#519)	Aug 22, 2024
RTLgenproof.v		RTLgenproof.v	Add From Coq to Require of standard library modules	May 5, 2025
RTLgenspec.v		RTLgenspec.v	Replace AST.rettype by AST.xtype	Jul 15, 2024
RTLtyping.v		RTLtyping.v	Replace AST.rettype by AST.xtype	Jul 15, 2024
Regalloc.ml		Regalloc.ml	Various improvements in the wording of diagnostics.	Aug 2, 2018
Registers.v		Registers.v	Add From Coq to Require of standard library modules	May 5, 2025
Renumber.v		Renumber.v	Updated PR by removing whitespaces. Bug 17450.	Oct 20, 2015
Renumberproof.v		Renumberproof.v	Update the back-end proofs to the new linking framework.	Mar 6, 2016
SelectDiv.vp		SelectDiv.vp	Hybrid 64bit/32bit PowerPC port	May 3, 2017
SelectDivproof.v		SelectDivproof.v	Add From Coq to Require of standard library modules	May 5, 2025
Selection.v		Selection.v	Add From Coq to Require of standard library modules	May 5, 2025
Selectionaux.ml		Selectionaux.ml	Selection: refined heuristic for if-conversion	Aug 22, 2024
Selectionproof.v		Selectionproof.v	Add From Coq to Require of standard library modules	May 5, 2025
SplitLong.vp		SplitLong.vp	Add From Coq to Require of standard library modules	May 5, 2025
SplitLongproof.v		SplitLongproof.v	Add From Coq to Require of standard library modules	May 5, 2025
Splitting.ml		Splitting.ml	Deactivate warning 27 and added back removed code.	Mar 15, 2016
Stacking.v		Stacking.v	Mgetparent -> Mgetparam	Aug 24, 2024
Stackingproof.v		Stackingproof.v	Simplify memory chunks in the Stacking pass	May 22, 2024
Tailcall.v		Tailcall.v	Replace AST.rettype by AST.xtype	Jul 15, 2024
Tailcallproof.v		Tailcallproof.v	Replace AST.rettype by AST.xtype	Jul 15, 2024
Tunneling.v		Tunneling.v	Add From Coq to Require of standard library modules	May 5, 2025
Tunnelingproof.v		Tunnelingproof.v	Add From Coq to Require of standard library modules	May 5, 2025
Unusedglob.v		Unusedglob.v	Add From Coq to Require of standard library modules	May 5, 2025
Unusedglobproof.v		Unusedglobproof.v	Add From Coq to Require of standard library modules	May 5, 2025
ValueAnalysis.v		ValueAnalysis.v	Add From Coq to Require of standard library modules	May 5, 2025
ValueDomain.v		ValueDomain.v	Add From Coq to Require of standard library modules	May 5, 2025
XTL.ml		XTL.ml	Use richer types rettype for function arguments in function signatures	Jul 15, 2024
XTL.mli		XTL.mli	Introduce register pairs to describe calling conventions more precisely	May 17, 2016
View all files