Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
CertiCompil
CompCert-KVX
Commits
706b6384
Commit
706b6384
authored
Mar 29, 2021
by
Léo Gourdin
Browse files
adding test for load replacement on a64
parent
3e953ef4
Changes
4
Hide whitespace changes
Inline
Side-by-side
test/gourdinl/clause.h
0 → 100644
View file @
706b6384
typedef
struct
{
int
b
;
int
a
;
}
*
CLAUSE
;
__inline__
int
g
(
CLAUSE
c
)
{
return
c
->
b
;
}
__inline__
int
d
(
CLAUSE
c
)
{
return
c
->
a
;
}
__inline__
void
clause_SetNumOfConsLits
(
CLAUSE
c
,
int
e
)
{
c
->
b
=
e
;
c
->
a
=
e
;
}
__inline__
int
f
(
CLAUSE
c
)
{
return
g
(
c
)
+
d
(
c
);
}
__inline__
int
clause_LastLitIndex
(
c
)
{
return
f
(
c
);
}
test/gourdinl/clause2.c
0 → 100644
View file @
706b6384
#include "clause.h"
int
a
,
b
;
void
c
();
void
h
()
{
int
f
=
clause_LastLitIndex
(
d
);
a
=
clause_LastLitIndex
(
0
);
if
(
f
)
if
(
a
)
1
;
}
void
i
()
{
CLAUSE
e
=
0
;
int
*
g
[]
=
{
h
,
c
};
for
(;
b
;)
l
(
e
);
}
void
m
()
{
int
k
,
j
;
for
(;
k
<=
0
;)
;
clause_SetNumOfConsLits
(
0
,
j
);
n
(
0
-
j
);
}
test/gourdinl/cscript.sh
0 → 100755
View file @
706b6384
#!/bin/bash
/home/yuki/Work/VERIMAG/Compcert_neutral/ccomp
-stdlib
../../runtime
-dparse
-dclight
-S
-fstruct-return
-c
clause2.c
>
log 2>&1
b1
=
$(
cat
log | ack
"LDP_CONSEC_PEEP_IMM_DEC_ldr64"
)
sb1
=
$?
b2
=
$(
cat
log | ack
"LDP_BACK_SPACED_PEEP_IMM_DEC_ldr32"
)
sb2
=
$?
b3
=
$(
cat
log | ack
"STP_FORW_SPACED_PEEP_IMM_INC_str32"
)
sb3
=
$?
b4
=
$(
cat
log | ack
"STP_CONSEC_PEEP_IMM_INC_str64"
)
sb4
=
$?
#if [ "$sb1" == 0 ] && [ "$sb2" == 0 ] && [ "$sb3" == 0 ] && [ "$sb4" == 0 ]
if
[
"
$sb1
"
==
0
]
&&
[
"
$sb2
"
==
0
]
&&
[
"
$sb3
"
==
0
]
&&
[
"
$sb4
"
==
0
]
then
exit
0
else
exit
1
fi
test/gourdinl/gen_asm_files.sh
0 → 100755
View file @
706b6384
#!/bin/bash
../../ccomp
-S
clause2.c
-o
clause2.nopostpass.noph.s
-fno-coalesce-mem
-fno-postpass
../../ccomp
-S
clause2.c
-o
clause2.nopostpass.ph.s
-fcoalesce-mem
-fno-postpass
../../ccomp
-S
clause2.c
-o
clause2.noph.s
-fno-coalesce-mem
../../ccomp
-S
clause2.c
-o
clause2.ph.s
-fcoalesce-mem
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment