aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* use all same exact include filesv3.5_k1c_1.2David Monniaux2019-06-032-26/+15
* Merge remote-tracking branch 'origin/mppa-work' into mppa-cosDavid Monniaux2019-05-3021-53/+891
|\
| * Merge remote-tracking branch 'origin/mppa-msub' into mppa-workDavid Monniaux2019-05-3022-54/+892
| |\
| | * standardization of expressionsDavid Monniaux2019-05-122-10/+8
| | * standardize semantics, 1David Monniaux2019-05-122-7/+12
| | * Merge remote-tracking branch 'origin/mppa-work' into mppa-msubDavid Monniaux2019-05-124-67/+88
| | |\
| | * | correct -faddx option and propagate addim over addximDavid Monniaux2019-05-114-10/+21
| | * | option -faddx (off by default until questions cleared)David Monniaux2019-05-118-29/+97
| | * | apply .xs onto addx4 etcDavid Monniaux2019-05-1110-27/+180
| | * | more maddxDavid Monniaux2019-05-112-0/+74
| | * | maddx ordre opposéDavid Monniaux2019-05-112-0/+6
| | * | add with shift, beginningDavid Monniaux2019-05-117-13/+86
| | * | generate multiply-sub longDavid Monniaux2019-05-113-4/+56
| | * | Pmsub compiledDavid Monniaux2019-05-119-40/+48
| | * | more gen O -> PDavid Monniaux2019-05-111-0/+9
| | * | more gen O -> PDavid Monniaux2019-05-111-0/+6
| | * | Oaddx -> PDavid Monniaux2019-05-115-21/+48
| | * | begin generating Prevsub etc. from Oxxx to PxxxDavid Monniaux2019-05-118-44/+47
| | * | use shift 1-4 in backendDavid Monniaux2019-05-105-97/+62
| | * | more integer OpDavid Monniaux2019-05-104-17/+245
| | * | new instructions at asm levelDavid Monniaux2019-05-105-9/+157
* | | | Merge branch 'mppa-cos' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2019-05-301-2/+3
|\ \ \ \
| * | | | make -j20 instead of xargs -P4 + make -j5Cyril SIX2019-05-291-2/+3
* | | | | take other measurementsDavid Monniaux2019-05-292-2/+2
|/ / / /
* | | | use /usr/bin/envDavid Monniaux2019-05-291-1/+1
* | | | Merge branch 'mppa-cos' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2019-05-290-0/+0
|\ \ \ \
| * | | | 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
|/ / / /
* | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cosDavid Monniaux2019-05-292-2/+3
|\| | |
| * | | 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
* | | | 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
|/ / /
* | | move Asmblockgenproof0 from lib to mppa_k1c/Sylvain Boulmé2019-05-211-0/+0
* | | move Machblock*.v into mppa_k1c/libSylvain Boulmé2019-05-213-0/+0
* | | Better graphsCyril SIX2019-05-211-37/+41
* | | 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
|\ \ \
| * | | 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