aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| | * | | Putting back the building rules for the paper (rules.mk)Cyril SIX2019-11-131-11/+11
| | * | | Removing clutter from building + running benchesCyril SIX2019-11-134-7/+21
| | * | | Merge remote-tracking branch 'origin/mppa-duplicate-rtl-alt' into mppa-workCyril SIX2019-10-242-60/+77
| | |\ \ \
| | | * | | An alternative proof where the match_state does not depend on the translationSylvain Boulmé2019-10-232-60/+77
| | * | | | Scaling down forgotten tests -> test/c/ operationalCyril SIX2019-10-227-3/+27
| | * | | | Un espace en tropCyril SIX2019-10-211-1/+1
| | * | | | Adding MPPA endianess in test/endian.hCyril SIX2019-10-211-1/+1
| | * | | | fix compile for rv32David Monniaux2019-10-161-0/+2
| | * | | | eq_condition already existedDavid Monniaux2019-10-163-8/+2
| | * | | | [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-1681-295/+16215
| | |\ \ \ \ | | | | |_|/ | | | |/| |
| | * | | | Few minor other changes in proofCyril SIX2019-10-151-3/+3
| | * | | | More elaborate comments + rewriting for easier to understand Asmblockgenproof.vCyril SIX2019-10-151-145/+89
| | * | | | Fix for test/regression/struct2.cCyril SIX2019-10-141-1/+2
| | * | | | Tackling struct passing by value for the future K1C ABICyril SIX2019-10-143-2/+12
| | * | | | Explicitly naming SP_split_args for easier greppingCyril SIX2019-10-141-1/+1
| | * | | | Converting mppa_k1c/*.v files to Unix formatCyril SIX2019-10-112-754/+754
| | * | | | Fixing fp_is_parent too weak (#165)Cyril SIX2019-10-112-1798/+1811
| * | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-2557-63/+437
| |\ \ \ \ \
| * | | | | | trapping ops on rvDavid Monniaux2019-09-241-0/+30
| * | | | | | trapping opsDavid Monniaux2019-09-241-0/+30
| * | | | | | trapping opsDavid Monniaux2019-09-241-0/+24
| * | | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-241-2/+2
| |\ \ \ \ \ \
| * | | | | | | add: non trapping opsDavid Monniaux2019-09-232-0/+57
| * | | | | | | is_trapping_op_soundDavid Monniaux2019-09-231-0/+28
| * | | | | | | Merge tag 'v3.6_mppa_2019-09-20' of gricad-gitlab.univ-grenoble-alpes.fr:sixc...David Monniaux2019-09-2083-297/+16313
| |\ \ \ \ \ \ \
| | * \ \ \ \ \ \ Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into mppa-workv3.6_mppa_2019-09-20David Monniaux2019-09-2086-300/+16263
| | |\ \ \ \ \ \ \ | | | | |_|_|_|_|/ | | | |/| | | | |
| | | * | | | | | fix compiling for aarch64David Monniaux2019-09-204-4/+42
| | | * | | | | | fix compilingDavid Monniaux2019-09-204-3/+8
| | | * | | | | | extraction problemsDavid Monniaux2019-09-202-2/+2
| | | * | | | | | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into mppa-work-upstrea...David Monniaux2019-09-2082-298/+16217
| | | |\ \ \ \ \ \ | | | | | |_|_|/ / | | | | |/| | | |
| | | | * | | | | Update for release 3.6v3.6Xavier Leroy2019-09-171-2/+3
| | | | * | | | | Revise the "bench" entries of the test suiteXavier Leroy2019-09-175-12/+110
| | | | * | | | | Updates in preparation for release 3.6Xavier Leroy2019-09-162-1/+63
| | | | * | | | | -dclight output: use nicer names for temporary variablesXavier Leroy2019-09-161-2/+11
| | | | * | | | | clightgen -dclight: print function parameters correctlyXavier Leroy2019-09-163-16/+35
| | | | * | | | | Reworked json export.Bernhard Schommer2019-09-125-78/+91
| | | | * | | | | Asmgenproof1: useless unfolding in proof scripts causing "omega" to failXavier Leroy2019-09-111-3/+3
| | | | * | | | | Merge pull request #313 from AbsInt/aarch64Xavier Leroy2019-09-1163-167/+15898
| | | | |\ \ \ \ \
| | | | | * | | | | AArch64: wrong expected type for arguments of Cmaskl{zero,notzero}xavier.leroy2019-08-312-4/+4
| | | | | * | | | | Offset out of range for ldp/stp instructionsxavier.leroy2019-08-231-1/+3
| | | | | * | | | | Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-176-16/+16
| | | | | * | | | | Test for the compilation of floating-point literalsXavier Leroy2019-08-083-1/+562
| | | | | * | | | | AArch64 portXavier Leroy2019-08-0848-87/+14874
| | | | | * | | | | Relax lemma Val.zero_ext_and and add Val.zero_ext_andlXavier Leroy2019-08-071-2/+10
| | | | | * | | | | Factor out endianness determination between testsXavier Leroy2019-08-074-30/+14
| | | | | * | | | | ndfun: add support for guards on patternsXavier Leroy2019-08-071-5/+16
| | | | | * | | | | More lemmas about powers of 2Xavier Leroy2019-08-071-0/+14
| | | | | * | | | | Errors: fixed a loop in tactic MonadInvXavier Leroy2019-08-071-1/+1
| | | | | * | | | | Asmgenproof0: add predicate exec_straight0Xavier Leroy2019-08-071-0/+26
| | | | | * | | | | Values: add functions for zero- and sign-extension of 64-bit integersXavier Leroy2019-08-071-0/+12
generated by cgit (git 2.34.1) at 2024-07-18 21:48:22 +0000