aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* copyright blockDavid Monniaux2019-05-291-0/+183
|
* Merge remote-tracking branch 'origin/mppa-cos' into mppa-fast-divDavid Monniaux2019-05-293-1/+3
|\
| * use /usr/bin/envDavid Monniaux2019-05-291-1/+1
| |
| * Merge branch 'mppa-cos' of ↵David Monniaux2019-05-290-0/+0
| |\ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-cos
| | * configure: typo fix in __K1C_$os__ -> __K1C_"$os"__ (was missing quotes)Cyril SIX2019-05-291-1/+1
| | |
| * | added some include filesDavid Monniaux2019-05-292-0/+2
| | |
| * | fix variable issueDavid Monniaux2019-05-291-1/+1
| |/
* | use silent FPDavid Monniaux2019-05-291-9/+9
| |
* | added -fdiv-i32 and -fdiv-i64 optionsDavid Monniaux2019-05-293-5/+20
| |
* | arranging for selection of divisor as optionDavid Monniaux2019-05-299-146/+89
| |
* | fixesDavid Monniaux2019-05-291-0/+1
| |
* | various fixesDavid Monniaux2019-05-292-1/+3
| |
* | Merge remote-tracking branch 'origin/mppa-cos' into mppa-fast-divDavid Monniaux2019-05-290-0/+0
|\|
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-cosDavid Monniaux2019-05-292-2/+3
| |\
* | | Merge remote-tracking branch 'origin/mppa-cos' into mppa-fast-divDavid Monniaux2019-05-2914-358/+53
|\| |
| * | to be able to use DDR we need 8-byte pointers in jump tablesDavid Monniaux2019-05-291-5/+5
| | |
| * | more builtinsDavid Monniaux2019-05-291-0/+2
| | |
| * | fixes for COSDavid Monniaux2019-05-282-0/+12
| | |
| * | adaptation pour k1c-cosDavid Monniaux2019-05-2812-354/+35
| | |
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-divDavid Monniaux2019-05-298-40/+45
|\ \ \ | | |/ | |/|
| * | error in the classification of SrswDavid Monniaux2019-05-291-2/+2
| | |
| * | Added rm clock.o and stuffCyril SIX2019-05-281-0/+1
| | |
| * | use /usr/bin/env bashDavid Monniaux2019-05-281-1/+1
| |/
| * move Asmblockgenproof0 from lib to mppa_k1c/Sylvain Boulmé2019-05-211-0/+0
| | | | | | | | This file is specific to our backend.
| * move Machblock*.v into mppa_k1c/libSylvain Boulmé2019-05-213-0/+0
| | | | | | | | Indeed, these files may not be specific to our backend.
| * Better graphsCyril SIX2019-05-211-37/+41
| |
* | new routines for 32-bit divisionDavid Monniaux2019-05-213-5/+122
| |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-divDavid Monniaux2019-05-217-949/+712
|\|
| * Added type annotations to gengraphs.pyCyril SIX2019-05-211-7/+8
| |
| * Added types annotations to genmake.pyCyril SIX2019-05-211-8/+9
| |
| * legere simplification de preuveSylvain Boulmé2019-05-201-29/+7
| |
| * Merge remote-tracking branch 'machblock/mppa_k1c' into mppa-workCyril SIX2019-05-205-934/+717
| |\ | | | | | | | | | | | | Conflicts: mppa_k1c/lib/Asmblockgenproof0.v
| | * transf_program_correct prooftvdd2019-05-201-91/+7
| | |
| | * mSylvain Boulmé2019-05-201-4/+10
| | |
| | * is_trans_code_monotonic prooftvdd2019-05-171-56/+120
| | |
| | * step_simu_cfi_step ??tvdd2019-05-151-3/+32
| | |
| | * mtvdd2019-05-151-2/+16
| | |
| | * star_step_simu_body_step prooftvdd2019-05-131-26/+40
| | |
| | * petite simplif de preuveSylvain Boulmé2019-04-191-62/+26
| | |
| | * step_simu_header prooftvdd2019-04-181-9/+10
| | |
| | * trans_code_decompose prooftvdd2019-04-111-1/+86
| | |
| | * cleaner separation between Asmgenproof and MachblockgenproofSylvain Boulmé2019-04-072-8/+29
| | |
| | * extract Machgen.trans_code stuff from AsmgenproofSylvain Boulmé2019-04-073-99/+65
| | |
| | * relecture is_header, is_body, is_exit + pattern de preuve trans_code_decomposeSylvain Boulmé2019-04-041-16/+29
| | |
| | * is_header, is_body, is_exittvdd2019-04-041-4/+16
| | |
| | * dist_end_block_code_simu_mid_block prooftvdd2019-04-041-1/+12
| | |
| | * bien meilleure façon de s'inspirer de l'ancienne traductionSylvain Boulmé2019-04-031-71/+59
| | |
| | * adaptation de quelques vieux lemmes pour la nouvelle traductionSylvain Boulmé2019-04-031-61/+84
| | |
| | * introduce a small tactic.Sylvain Boulmé2019-04-031-4/+7
| | |
| | * legeres simplificationsSylvain Boulmé2019-04-021-239/+42
| | |
generated by cgit (git 2.34.1) at 2024-07-14 05:56:07 +0000