Files

 master

/

x86

/

Copy path

Directory actions

More options

Directory actions

More options

Latest commit

xavierleroy

x86: wrong modeling of ZF flag for FP comparisons

Dec 20, 2018

50fd8fe · Dec 20, 2018

History

History

This branch is 703 commits behind AbsInt/CompCert:master.

/

x86

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
Asm.v		Asm.v	x86: wrong modeling of ZF flag for FP comparisons	Dec 20, 2018
AsmToJSON.ml		AsmToJSON.ml	Change AsmToJson to be similar to other printers.	Jan 5, 2018
AsmToJSON.mli		AsmToJSON.mli	Change AsmToJson to be similar to other printers.	Jan 5, 2018
Asmexpand.ml		Asmexpand.ml	Generate a nop instruction after some ais annotations (AbsInt#137)	Sep 12, 2018
Asmgen.v		Asmgen.v	In "symbol + ofs" addressing modes, limit the range of "ofs" in 64 bits	Feb 12, 2018
Asmgenproof.v		Asmgenproof.v	Model external calls as destroying all caller-save registers	Jun 1, 2018
Asmgenproof1.v		Asmgenproof1.v	x86: wrong modeling of ZF flag for FP comparisons	Dec 20, 2018
CBuiltins.ml		CBuiltins.ml	Moved common buitlins to C2C gernic_builtins.	Sep 26, 2017
CombineOp.v		CombineOp.v	Make Archi.ptr64 always computable, and reorganize files accordingly:…	Oct 27, 2016
CombineOpproof.v		CombineOpproof.v	Ensure FunInd or Recdef is imported if functional induction is used	Jul 20, 2017
ConstpropOp.vp		ConstpropOp.vp	Improve strength reduction of unsigned comparisons x ==u 0, x !=u 0, …	Feb 16, 2018
ConstpropOpproof.v		ConstpropOpproof.v	Improve strength reduction of unsigned comparisons x ==u 0, x !=u 0, …	Feb 16, 2018
Conventions1.v		Conventions1.v	Remove coq warnings (AbsInt#28)	Sep 22, 2017
Machregs.v		Machregs.v	New support for inserting ais-annotations.	Oct 19, 2017
Machregsaux.ml		Machregsaux.ml	Make Archi.ptr64 always computable, and reorganize files accordingly:…	Oct 27, 2016
Machregsaux.mli		Machregsaux.mli	Make Archi.ptr64 always computable, and reorganize files accordingly:…	Oct 27, 2016
NeedOp.v		NeedOp.v	Hybrid 64bit/32bit PowerPC port	May 3, 2017
Op.v		Op.v	In "symbol + ofs" addressing modes, limit the range of "ofs" in 64 bits	Feb 12, 2018
PrintOp.ml		PrintOp.ml	Make Archi.ptr64 always computable, and reorganize files accordingly:…	Oct 27, 2016
SelectLong.vp		SelectLong.vp	Make Archi.ptr64 always computable, and reorganize files accordingly:…	Oct 27, 2016
SelectLongproof.v		SelectLongproof.v	Hybrid 64bit/32bit PowerPC port	May 3, 2017
SelectOp.vp		SelectOp.vp	Extend builtin arguments with a pointer addition operator	Jul 6, 2017
SelectOpproof.v		SelectOpproof.v	Extend builtin arguments with a pointer addition operator	Jul 6, 2017
Stacklayout.v		Stacklayout.v	Remove coq warnings (AbsInt#28)	Sep 22, 2017
TargetPrinter.ml		TargetPrinter.ml	Generate a nop instruction after some ais annotations (AbsInt#137)	Sep 12, 2018
ValueAOp.v		ValueAOp.v	Make Archi.ptr64 always computable, and reorganize files accordingly:…	Oct 27, 2016
extractionMachdep.v		extractionMachdep.v	Resynchronize the LICENSE file and the license headers in individual …	Jan 5, 2018
View all files