aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* not yet the transfer functions that record predicatesDavid Monniaux2020-11-263-9/+78
* remains one admitDavid Monniaux2020-11-261-8/+46
* is_condition_present_soundDavid Monniaux2020-11-263-5/+23
* begin implementing cond tableDavid Monniaux2020-11-261-6/+13
* ajouté Cond, tout passeDavid Monniaux2020-11-263-40/+168
* passage à EquDavid Monniaux2020-11-264-190/+197
* op_depends_on_memory_correctDavid Monniaux2020-11-251-6/+24
* cond_valid_pointer_eqDavid Monniaux2020-11-256-0/+64
* cond_valid_pointer_eqDavid Monniaux2020-11-251-5/+13
* store2_soundDavid Monniaux2020-11-251-1/+1
* clever_kill_store_soundDavid Monniaux2020-11-251-7/+5
* kill_store_soundDavid Monniaux2020-11-251-0/+49
* two lemmas admittedDavid Monniaux2020-11-253-9/+115
* missing lemmasDavid Monniaux2020-11-251-0/+21
* pointer_eq copiedDavid Monniaux2020-11-256-0/+86
* tiny simplification in Tunnelingaux.mlSylvain Boulmé2020-11-241-2/+2
* bug #223 fix on PPCDavid Monniaux2020-11-232-3/+73
* bug #223 fix for ARMDavid Monniaux2020-11-232-3/+76
* bug #223 fix on x86 / x86-64David Monniaux2020-11-232-4/+80
* fix wrong version of file on AArch64David Monniaux2020-11-231-1/+4
* Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2020-11-232-3/+14
|\
| * fix bug #223 on Risc-VDavid Monniaux2020-11-232-3/+14
* | fix bug #223 on AArch64David Monniaux2020-11-231-3/+72
|/
* correction bug #223 sur KVXDavid Monniaux2020-11-232-12/+22
* for 2010-11-18 Kalray releaseDavid Monniaux2020-11-191-1/+1
* minor fix in coq2html commentSylvain Boulmé2020-11-161-1/+2
* Tunneling: improved elimination of conditionsSylvain Boulmé2020-11-166-259/+673
* Proof of UnionFind.pathlen_unionSylvain Boulmé2020-11-161-10/+53
* Fixing issue with loops having branches leading to goto backedgeCyril SIX2020-11-052-27/+32
* Fixing get_loop_headers + alternative get_inner_loops (commented, not active)Cyril SIX2020-11-042-27/+107
* Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2020-11-041-1/+2
|\
| * youtube linkSylvain Boulmé2020-11-041-1/+2
| * Revert "Embed the short video with subtitles..."Sylvain Boulmé2020-11-041-10/+2
| * Embed the short video with subtitles...Sylvain Boulmé2020-11-041-2/+10
* | move loop rotate downDavid Monniaux2020-11-041-4/+5
* | do not print "refining" unless askedDavid Monniaux2020-11-041-1/+2
|/
* do not print "updates" to nodesDavid Monniaux2020-11-041-1/+2
* refixcse3David Monniaux2020-11-032-34/+53
* Loop Rotate with -flooprotateCyril SIX2020-11-035-1/+67
* refining CSE3 nodesDavid Monniaux2020-10-313-14/+84
* seems to work betterDavid Monniaux2020-10-312-3/+37
* also match IstoreDavid Monniaux2020-10-301-1/+2
* reinstated old versionDavid Monniaux2020-10-304-216/+39
* reinstated previous forward_move functionDavid Monniaux2020-10-292-11/+98
* CSE3 trivial_ops flagDavid Monniaux2020-10-292-3/+3
* in CSE3 choose lowest variable as representative for movesDavid Monniaux2020-10-294-45/+106
* deactivate LICMDavid Monniaux2020-10-281-1/+1
* DuplicateParam -> DuplicateOracle + simpler DuplicatepassesSylvain Boulmé2020-10-283-40/+24
* restore URL on the coqdocSylvain Boulmé2020-10-281-2/+3
* Correcting typoCyril SIX2020-10-271-3/+3
generated by cgit (git 2.34.1) at 2024-07-11 21:06:11 +0000