index
:
compcert-kvx
CPP22_if_lifting
CPP22_main
master
patched_for_velus
riscV-cmov
ssa
vericert
vericert-kvx
Unnamed repository; edit this file 'description' to name the repository.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
common
Commit message (
Expand
)
Author
Age
Files
Lines
*
Add Genv.public_symbol operation.
Xavier Leroy
2014-11-24
4
-180
/
+342
*
Record public global definitions via field "prog_public" in AST.program.
Xavier Leroy
2014-11-24
1
-3
/
+25
*
Excessively strict validation: ofs + sz < modulus should have been
xleroy
2014-08-20
1
-4
/
+5
*
Issue with switch labels that are negative 32-bit integers.
xleroy
2014-08-17
1
-0
/
+35
*
- Support "switch" statements over 64-bit integers
xleroy
2014-08-17
2
-171
/
+264
*
Add Mem.free_parallel_inject and use it to simplify Events a bit.
xleroy
2014-07-31
3
-35
/
+50
*
Update "read_as_zeros" property.
xleroy
2014-07-23
1
-1
/
+3
*
Merge of "newspilling" branch:
xleroy
2014-07-23
8
-504
/
+602
*
Add "read_as_zero" property for memory areas initialized by Init_space.
xleroy
2014-06-30
1
-14
/
+106
*
Refactoring: move symbol_offset into Genv.
xleroy
2014-05-24
1
-0
/
+17
*
Merge of branch linear-typing:
xleroy
2014-04-06
1
-0
/
+435
*
Revert commits r2435 and r2436 (coarser RTLtyping / finer Lineartyping):
xleroy
2014-03-28
1
-435
/
+0
*
Revised division of labor between RTLtyping and Lineartyping:
xleroy
2014-03-27
1
-0
/
+435
*
Type-checking of builtin volatile write Mfloat32 was too strict, causing type...
xleroy
2014-03-24
2
-4
/
+4
*
- Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.
xleroy
2014-01-12
5
-23
/
+16
*
Introduce and use the platform-specific Archi module giving:
xleroy
2014-01-03
2
-26
/
+26
*
Ctypes.sizeof ty = 0 for empty types ty (zero-sized array, empty struct/union).
xleroy
2013-12-30
2
-21
/
+111
*
Simpler, more robust emulation of calls to variadic functions:
xleroy
2013-12-28
2
-26
/
+44
*
Merge of branch value-analysis.
xleroy
2013-12-20
3
-68
/
+157
*
Revised semantics of external functions, continued:
xleroy
2013-11-18
1
-3
/
+10
*
Revised modeling of external functions and built-in functions: just axiomatize
xleroy
2013-11-17
1
-114
/
+25
*
powerpc/: new unary operation "addsymbol"
xleroy
2013-11-17
2
-18
/
+28
*
Cminor parsing and printing (from Andrew Tolmach)
xleroy
2013-10-16
1
-4
/
+4
*
Merge of Flocq version 2.2.0.
xleroy
2013-08-02
1
-5
/
+0
*
Alternate characterization of alignment constraints in memory injection, whic...
xleroy
2013-07-31
1
-107
/
+108
*
Optimize integer divisions by positive constants, turning them into
xleroy
2013-07-29
1
-0
/
+12
*
More accurate model of condition register flags for ARM and IA32.
xleroy
2013-07-13
1
-0
/
+12
*
Treat casts int64 -> float32 as primitive operations instead of two
xleroy
2013-07-03
1
-0
/
+12
*
Merge of the "princeton" branch:
xleroy
2013-06-16
5
-613
/
+689
*
Merge of the float32 branch:
xleroy
2013-05-19
6
-43
/
+967
*
Refactoring: move definition of chunk_of_type to AST.v.
xleroy
2013-05-06
1
-0
/
+10
*
Coq-defined equality functions for Allocation.
xleroy
2013-05-01
1
-3
/
+20
*
Expand 64-bit integer comparisons into 32-bit integer comparisons.
xleroy
2013-04-29
1
-4
/
+4
*
Big merge of the newregalloc-int64 branch. Lots of changes in two directions:
xleroy
2013-04-20
8
-70
/
+741
*
Glasnost: making transparent a number of definitions that were opaque
xleroy
2013-03-10
3
-22
/
+22
*
Assorted cleanups, esp. to avoid generating _rec and _rect recursors in
xleroy
2013-03-09
3
-51
/
+79
*
Constant propagation within __builtin_annot.
xleroy
2013-02-24
2
-9
/
+30
*
Pointers one past
xleroy
2013-02-15
4
-65
/
+334
*
Updated PowerPC port to new integers.
xleroy
2013-02-12
1
-1
/
+1
*
lib/Integers.v: revised and extended, faster implementation based on
xleroy
2013-02-10
2
-23
/
+24
*
Ported to Coq 8.4pl1. Merge of branches/coq-8.4.
xleroy
2013-01-29
5
-66
/
+66
*
Updated documentation
v1.12
xleroy
2013-01-11
1
-1
/
+1
*
Update Cminor parser and printer so that the parser can parse the whole Cmino...
xleroy
2013-01-07
1
-4
/
+4
*
Remove some useless "Require".
xleroy
2012-12-30
4
-4
/
+0
*
Merge of the clightgen branch:
xleroy
2012-12-29
1
-1
/
+1
*
Composition properties between injections and extensions.
xleroy
2012-12-29
1
-8
/
+80
*
Integers: specialized function to compute x mod 2^N; used in "repr" to
xleroy
2012-12-21
1
-1
/
+2
*
Support for inline assembly (asm statements).
xleroy
2012-12-18
3
-1
/
+12
*
Globalenvs: allocate one-byte block with permissions Nonempty for each
xleroy
2012-11-12
2
-1227
/
+979
*
Remove Val.is_true and Val.is_false, no longer used.
xleroy
2012-08-06
1
-67
/
+62
[next]