Skip to content

GitLab

Commit 4321731e authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Remove unused frontend tests.

parent 7158d4dd
Pipeline #50698 passed with stage
in 16 minutes and 37 seconds
Hide whitespace changes
Inline Side-by-side
frontend/tests/array.c deleted 100644 → 0
View file @ 7158d4dd
struct S {int i; int b[2]; int *c; int (*d)[]; };
int main() {
struct S nested[1][2];
struct S a[5];
struct S b;
struct S *c;
struct S (*d)[];
struct S (*f)[5];
// note that there is only use, no ! in the generated code (gets
// canceled by the array decay)
a[0];
a[0].i;
b.i;
c->i;
// the following two should generate identical code
(c + 0)->i;
(a + 0)->i;
// the following two should generate identical code
(*d)[0].i;
(*f)[0].i;
a[0].i = 1;
return 0;
}
// all arguments should have LPtr layout
int test(int a[2], int b[], int *c){
return 0;
}
frontend/tests/array_code.v deleted 100644 → 0
View file @ 7158d4dd
From refinedc.lang Require Export notation.
From refinedc.lang Require Import tactics.
From refinedc.typing Require Import annotations.
Set Default Proof Using "Type".
(* Generated from [examples/array.c]. *)
Section code.
(* Global variables. *)
(* Functions. *)
Context (main : loc).
Context (test : loc).
(* Definition of struct [S]. *)
Program Definition struct_S := {|
sl_members := [
("i", it_layout i32);
("b", mk_array_layout (it_layout i32) 2);
("c", LPtr);
("d", LPtr)
];
|}.
Solve Obligations with solve_struct_obligations.
(* Definition of function [main]. *)
Definition impl_main : function := {|
f_args := [
];
f_local_vars := [
("c", LPtr);
("f", LPtr);
("d", LPtr);
("b", layout_of struct_S);
("nested", mk_array_layout (mk_array_layout (layout_of struct_S) 2) 1);
("a", mk_array_layout (layout_of struct_S) 5)
];
f_init := "#0";
f_code := (
<[ "#0" :=
expr: (use{layout_of struct_S} (("a") at_offset{layout_of struct_S, PtrOp, IntOp i32} (i2v 0 i32))) ;
expr: (use{it_layout i32} ((("a") at_offset{layout_of struct_S, PtrOp, IntOp i32} (i2v 0 i32)) at{struct_S} "i")) ;
expr: (use{it_layout i32} (("b") at{struct_S} "i")) ;
expr: (use{it_layout i32} ((!{LPtr} ("c")) at{struct_S} "i")) ;
expr: (use{it_layout i32} ((!{LPtr} (("c") at_offset{layout_of struct_S, PtrOp, IntOp i32} (i2v 0 i32))) at{struct_S} "i")) ;
expr: (use{it_layout i32} ((!{LPtr} (("a") at_offset{layout_of struct_S, PtrOp, IntOp i32} (i2v 0 i32))) at{struct_S} "i")) ;
expr: (use{it_layout i32} (((!{LPtr} ("d")) at_offset{layout_of struct_S, PtrOp, IntOp i32} (i2v 0 i32)) at{struct_S} "i")) ;
expr: (use{it_layout i32} (((!{LPtr} ("f")) at_offset{layout_of struct_S, PtrOp, IntOp i32} (i2v 0 i32)) at{struct_S} "i")) ;
(("a") at_offset{layout_of struct_S, PtrOp, IntOp i32} (i2v 0 i32)) at{struct_S} "i" <-{ it_layout i32 }
i2v 1 i32 ;
Return (i2v 0 i32)
]> $∅
)%E
|}.
(* Definition of function [test]. *)
Definition impl_test : function := {|
f_args := [
("a", LPtr);
("b", LPtr);
("c", LPtr)
];
f_local_vars := [
];
f_init := "#0";
f_code := (
<[ "#0" :=
Return (i2v 0 i32)
]> $∅
)%E
|}.
End code.
frontend/tests/control_flow.c deleted 100644 → 0
View file @ 7158d4dd
int main() {
int toplevel, i;
if (1) {
int nested;
1;
}
while(1){2;}
// TODO: support declaring variables here?
for(i = 0; i < toplevel; i += 1) {
3;
}
// TODO: support || and &&
// if (1 || 2 && 3) {}
}
frontend/tests/control_flow_code.v deleted 100644 → 0
View file @ 7158d4dd
From refinedc.lang Require Export notation.
From refinedc.lang Require Import tactics.
From refinedc.typing Require Import annotations.
Set Default Proof Using "Type".
(* Generated from [examples/control_flow.c]. *)
Section code.
(* Global variables. *)
(* Functions. *)
Context (main : loc).
(* Definition of function [main]. *)
Definition impl_main : function := {|
f_args := [
];
f_local_vars := [
("i", it_layout i32);
("toplevel", it_layout i32);
("nested", it_layout i32)
];
f_init := "#0";
f_code := (
<[ "#0" :=
if: UnOp (CastOp $ IntOp bool_it) (IntOp i32) (i2v 1 i32)
then
expr: (i2v 1 i32) ;
Goto "#5"
else
Goto "#5"
]> $
<[ "#1" :=
if: UnOp (CastOp $ IntOp bool_it) (IntOp i32) (i2v 1 i32)
then
expr: (i2v 2 i32) ;
Goto "continue3"
else
Goto "#2"
]> $
<[ "#2" :=
"i" <-{ it_layout i32 } i2v 0 i32 ;
Goto "#3"
]> $
<[ "#3" :=
if: UnOp (CastOp $ IntOp bool_it) (IntOp i32) ((use{it_layout i32} ("i")) <{IntOp i32, IntOp i32} (use{it_layout i32} ("toplevel")))
then
expr: (i2v 3 i32) ;
Goto "continue5"
else
Goto "#4"
]> $
<[ "#4" :=
Return (VOID)
]> $
<[ "#5" :=
Goto "#1"
]> $
<[ "continue3" :=
Goto "#1"
]> $
<[ "continue5" :=
"i" <-{ it_layout i32 }
(use{it_layout i32} ("i")) +{IntOp i32, IntOp i32} (i2v 1 i32) ;
Goto "#3"
]> $∅
)%E
|}.
End code.
frontend/tests/int.c deleted 100644 → 0
View file @ 7158d4dd
#include <stdbool.h>
#include <stddef.h>
#include <stdint.h>
long f(int i, char c){
return i;
}
int main() {
unsigned char uc; signed char sc; char c;
unsigned short us; signed short ss; short s;
unsigned int ui; signed int si; int i;
unsigned long ul; signed long sl; long l;
unsigned long long ull; signed long long sll; long long ll;
_Bool b;
size_t st; uintptr_t uptr; intptr_t ptr;
int *iptr;
c = 0;
// test constant modifiers
ull = 0L;
ull = 0LL;
ull = 0ULL;
ull = 0UL;
// test promotion
i = c + c;
// test conversion
i = i + ull;
// test casts
i = (char) ll;
// test boolean
b = true;
b = false;
b = l == l;
// the following is not allowed intentionally
// b = i == l;
b = (long)i == l;
b = l + l;
b = i + l;
// test if stmt and assert
if (l == l) {
assert(l == l);
}
// test function call
i = f(c, l);
(void *)iptr;
return 0;
}
frontend/tests/int_code.v deleted 100644 → 0
View file @ 7158d4dd
From refinedc.lang Require Export notation.
From refinedc.lang Require Import tactics.
From refinedc.typing Require Import annotations.
Set Default Proof Using "Type".
(* Generated from [examples/int.c]. *)
Section code.
(* Global variables. *)
(* Functions. *)
Context (f : loc).
Context (main : loc).
(* Definition of function [f]. *)
Definition impl_f : function := {|
f_args := [
("i", it_layout i32);
("c", it_layout u8)
];
f_local_vars := [
];
f_init := "#0";
f_code := (
<[ "#0" :=
Return (UnOp (CastOp $ IntOp i64) (IntOp i32) (use{it_layout i32} ("i")))
]> $∅
)%E
|}.
(* Definition of function [main]. *)
Definition impl_main : function := {|
f_args := [
];
f_local_vars := [
("i", it_layout i32);
("c", it_layout u8);
("ull", it_layout u64);
("sc", it_layout i8);
("sll", it_layout i64);
("uc", it_layout u8);
("us", it_layout u16);
("ui", it_layout u32);
("uptr", it_layout size_t);
("s", it_layout i16);
("sl", it_layout i64);
("ll", it_layout i64);
("ss", it_layout i16);
("si", it_layout i32);
("l", it_layout i64);
("ul", it_layout u64);
("iptr", LPtr);
("st", it_layout size_t);
("ptr", it_layout ssize_t);
("b", it_layout bool_it)
];
f_init := "#0";
f_code := (
<[ "#0" :=
"c" <-{ it_layout u8 }
UnOp (CastOp $ IntOp u8) (IntOp i32) (i2v 0 i32) ;
"ull" <-{ it_layout u64 }
UnOp (CastOp $ IntOp u64) (IntOp i64) (i2v 0 i64) ;
"ull" <-{ it_layout u64 }
UnOp (CastOp $ IntOp u64) (IntOp i64) (i2v 0 i64) ;
"ull" <-{ it_layout u64 } i2v 0 u64 ;
"ull" <-{ it_layout u64 } i2v 0 u64 ;
"i" <-{ it_layout i32 }
(UnOp (CastOp $ IntOp i32) (IntOp u8) (use{it_layout u8} ("c"))) +{IntOp i32, IntOp i32} (UnOp (CastOp $ IntOp i32) (IntOp u8) (use{it_layout u8} ("c"))) ;
"i" <-{ it_layout i32 }
UnOp (CastOp $ IntOp i32) (IntOp u64) ((UnOp (CastOp $ IntOp u64) (IntOp i32) (use{it_layout i32} ("i"))) +{IntOp u64, IntOp u64} (use{it_layout u64} ("ull"))) ;
"i" <-{ it_layout i32 }
UnOp (CastOp $ IntOp i32) (IntOp u8) (UnOp (CastOp $ IntOp u8) (IntOp i64) (use{it_layout i64} ("ll"))) ;
"b" <-{ it_layout bool_it }
UnOp (CastOp $ IntOp bool_it) (IntOp i32) (i2v 1 i32) ;
"b" <-{ it_layout bool_it }
UnOp (CastOp $ IntOp bool_it) (IntOp i32) (i2v 0 i32) ;
"b" <-{ it_layout bool_it }
UnOp (CastOp $ IntOp bool_it) (IntOp i32) ((use{it_layout i64} ("l")) ={IntOp i64, IntOp i64} (use{it_layout i64} ("l"))) ;
"b" <-{ it_layout bool_it }
UnOp (CastOp $ IntOp bool_it) (IntOp i32) ((UnOp (CastOp $ IntOp i64) (IntOp i32) (use{it_layout i32} ("i"))) ={IntOp i64, IntOp i64} (use{it_layout i64} ("l"))) ;
"b" <-{ it_layout bool_it }
UnOp (CastOp $ IntOp bool_it) (IntOp i64) ((use{it_layout i64} ("l")) +{IntOp i64, IntOp i64} (use{it_layout i64} ("l"))) ;
"b" <-{ it_layout bool_it }
UnOp (CastOp $ IntOp bool_it) (IntOp i64) ((UnOp (CastOp $ IntOp i64) (IntOp i32) (use{it_layout i32} ("i"))) +{IntOp i64, IntOp i64} (use{it_layout i64} ("l"))) ;
if: UnOp (CastOp $ IntOp bool_it) (IntOp i32) ((use{it_layout i64} ("l")) ={IntOp i64, IntOp i64} (use{it_layout i64} ("l")))
then
assert: (UnOp (CastOp $ IntOp bool_it) (IntOp i32) ((use{it_layout i64} ("l")) ={IntOp i64, IntOp i64} (use{it_layout i64} ("l")))) ;
Goto "#1"
else
Goto "#1"
]> $
<[ "#1" :=
"$0" <- f with
[ UnOp (CastOp $ IntOp i32) (IntOp u8) (use{it_layout u8} ("c")) ;
UnOp (CastOp $ IntOp u8) (IntOp i64) (use{it_layout i64} ("l")) ] ;
"i" <-{ it_layout i32 }
UnOp (CastOp $ IntOp i32) (IntOp i64) ("$0") ;
expr: (UnOp (CastOp $ PtrOp) (PtrOp) (use{LPtr} ("iptr"))) ;
Return (i2v 0 i32)
]> $∅
)%E
|}.
End code.
frontend/tests/loop_annot.c deleted 100644 → 0
View file @ 7158d4dd
int main() {
int i;
[[rc::inv_vars("i : int")]]
while(1){
i = i + 1;
}
[[rc::inv_vars("i : int")]]
do {
i = i + 1;
} while(1);
return 0;
}
frontend/tests/loop_annot_code.v deleted 100644 → 0
View file @ 7158d4dd
From refinedc.lang Require Export notation.
From refinedc.lang Require Import tactics.
From refinedc.typing Require Import annotations.
Set Default Proof Using "Type".
(* Generated from [examples/loop_annot.c]. *)
Section code.
(* Global variables. *)
(* Functions. *)
Context (main : loc).
(* Definition of function [main]. *)
Definition impl_main : function := {|
f_args := [
];
f_local_vars := [
("i", it_layout i32)
];
f_init := "#0";
f_code := (
<[ "#0" :=
Goto "#1"
]> $
<[ "#1" :=
if: UnOp (CastOp $ IntOp bool_it) (IntOp i32) (i2v 1 i32)
then
"i" <-{ it_layout i32 }
(use{it_layout i32} ("i")) +{IntOp i32, IntOp i32} (i2v 1 i32) ;
Goto "continue2"
else
Goto "#2"
]> $
<[ "#2" :=
Goto "#3"
]> $
<[ "#3" :=
"i" <-{ it_layout i32 }
(use{it_layout i32} ("i")) +{IntOp i32, IntOp i32} (i2v 1 i32) ;
Goto "continue4"
]> $
<[ "#4" :=
Return (i2v 0 i32)
]> $
<[ "continue2" :=
Goto "#1"
]> $
<[ "continue4" :=
if: UnOp (CastOp $ IntOp bool_it) (IntOp i32) (i2v 1 i32)
then
Goto "#3"
else
Goto "#4"
]> $∅
)%E
|}.
End code.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment