From e586380e632ef112fcf60a6cb413ae82a23d3b32 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Mon, 4 Sep 2023 10:16:34 +0200
Subject: [PATCH] Add test and oracle for access to array field of
struct-returning fun
---
...emporary_object_issue_1037-1220.res.oracle | 269 ++++++++++++++++++
.../syntax/temporary_object_issue_1037-1220.i | 93 ++++++
2 files changed, 362 insertions(+)
create mode 100644 tests/syntax/oracle/temporary_object_issue_1037-1220.res.oracle
create mode 100644 tests/syntax/temporary_object_issue_1037-1220.i
diff --git a/tests/syntax/oracle/temporary_object_issue_1037-1220.res.oracle b/tests/syntax/oracle/temporary_object_issue_1037-1220.res.oracle
new file mode 100644
index 00000000000..b25ba284ac5
--- /dev/null
+++ b/tests/syntax/oracle/temporary_object_issue_1037-1220.res.oracle
@@ -0,0 +1,269 @@
+[kernel] Parsing temporary_object_issue_1037-1220.i (no preprocessing)
+/* Generated by Frama-C */
+struct X {
+ int arr[1] ;
+};
+struct S {
+ struct X x ;
+};
+struct X get_x(void)
+{
+ struct X __constr_expr_0 = {.arr = {42}};
+ return __constr_expr_0;
+}
+
+struct S get_s(void)
+{
+ struct S __constr_expr_1 = {.x = {.arr = {42}}};
+ return __constr_expr_1;
+}
+
+int init(void)
+{
+ int __retres;
+ int *tmp_0;
+ int const *tmp_3;
+ {
+ struct X tmp;
+ tmp = get_x();
+ tmp_0 = tmp.arr;
+ }
+ int *p = tmp_0;
+ {
+ struct X tmp_1;
+ tmp_1 = get_x();
+ p = tmp_1.arr;
+ }
+ {
+ struct X tmp_2;
+ tmp_2 = get_x();
+ tmp_3 = (int const *)(tmp_2.arr);
+ }
+ int const *q = tmp_3;
+ __retres = *p + *q;
+ return __retres;
+}
+
+int g1(int *x)
+{
+ int __retres;
+ __retres = *x;
+ return __retres;
+}
+
+void g2(int *x)
+{
+ *x = 1;
+ return;
+}
+
+void calls(void)
+{
+ int tmp_0;
+ {
+ struct X tmp;
+ tmp = get_x();
+ tmp_0 = g1(tmp.arr);
+ }
+ int d = tmp_0;
+ {
+ struct X tmp_1;
+ tmp_1 = get_x();
+ g2(tmp_1.arr);
+ }
+ return;
+}
+
+int *cond(void)
+{
+ int *__retres;
+ char *tmp_1;
+ int tmp_3;
+ int *tmp_7;
+ {
+ struct X tmp;
+ tmp = get_x();
+ }
+ {
+ struct X tmp_0;
+ tmp_0 = get_x();
+ tmp_1 = (char *)(tmp_0.arr);
+ }
+ if (tmp_1) {
+ __retres = (int *)1;
+ goto return_label;
+ }
+ {
+ struct X tmp_2;
+ tmp_2 = get_x();
+ ;
+ tmp_3 = tmp_2.arr[0];
+ }
+ if (tmp_3) {
+ __retres = (int *)2;
+ goto return_label;
+ }
+ {
+ int i = 0;
+ while (1) {
+ {
+ struct X tmp_4;
+ tmp_4 = get_x();
+ if (! (tmp_4.arr)) break;
+ }
+ i ++;
+ }
+ }
+ while (1) {
+ {
+ struct X tmp_5;
+ tmp_5 = get_x();
+ if (! (tmp_5.arr)) break;
+ }
+ }
+ {
+ struct X tmp_6;
+ tmp_6 = get_x();
+ tmp_7 = tmp_6.arr;
+ }
+ __retres = tmp_7;
+ return_label: return __retres;
+}
+
+int paren_return(void)
+{
+ int __retres;
+ int *tmp_2;
+ int tmp_4;
+ {
+ struct X tmp;
+ tmp = get_x();
+ }
+ {
+ struct X tmp_0;
+ tmp_0 = get_x();
+ }
+ {
+ struct X tmp_1;
+ tmp_1 = get_x();
+ tmp_2 = tmp_1.arr;
+ }
+ if (tmp_2) {
+ __retres = 1;
+ goto return_label;
+ }
+ {
+ struct X tmp_3;
+ tmp_3 = get_x();
+ tmp_4 = tmp_3.arr[0];
+ }
+ __retres = tmp_4;
+ return_label: return __retres;
+}
+
+int nested(void)
+{
+ int __retres;
+ int *tmp_0;
+ int *tmp_2;
+ int tmp_4;
+ {
+ struct S tmp;
+ tmp = get_s();
+ tmp_0 = tmp.x.arr;
+ }
+ int *p = tmp_0;
+ {
+ struct S tmp_1;
+ tmp_1 = get_s();
+ tmp_2 = tmp_1.x.arr;
+ }
+ if (tmp_2) {
+ __retres = 1;
+ goto return_label;
+ }
+ {
+ struct S tmp_3;
+ tmp_3 = get_s();
+ tmp_4 = g1(tmp_3.x.arr);
+ }
+ int d = tmp_4;
+ __retres = *p;
+ return_label: return __retres;
+}
+
+int f(void)
+{
+ int __retres;
+ __retres = 1;
+ return __retres;
+}
+
+int comma(void)
+{
+ int __retres;
+ int *p;
+ int *q;
+ int tmp_0;
+ int tmp_3;
+ int tmp_8;
+ {
+ struct X tmp;
+ tmp = get_x();
+ p = tmp.arr;
+ tmp_0 = *p;
+ }
+ int x = tmp_0;
+ int y = *p;
+ {
+ struct X tmp_1;
+ struct X tmp_2;
+ tmp_1 = get_x();
+ p = tmp_1.arr;
+ tmp_2 = get_x();
+ q = tmp_2.arr;
+ tmp_3 = *p + *q;
+ }
+ if (tmp_3) {
+ __retres = *p + *q;
+ goto return_label;
+ }
+ while (1) {
+ {
+ struct X tmp_4;
+ tmp_4 = get_x();
+ p = tmp_4.arr;
+ if (! *p) break;
+ }
+ __retres = *p;
+ goto return_label;
+ }
+ while (1) {
+ {
+ struct X tmp_5;
+ tmp_5 = get_x();
+ p = tmp_5.arr;
+ if (*p) {
+ int tmp_6;
+ tmp_6 = f();
+ if (! tmp_6) break;
+ }
+ else break;
+ }
+ __retres = *p;
+ goto return_label;
+ }
+ {
+ struct X tmp_7;
+ tmp_7 = get_x();
+ p = tmp_7.arr;
+ if (*p)
+ if (*p) tmp_8 = 1; else tmp_8 = 0;
+ else tmp_8 = 0;
+ }
+ int d = tmp_8;
+ __retres = y;
+ return_label: return __retres;
+}
+
+
diff --git a/tests/syntax/temporary_object_issue_1037-1220.i b/tests/syntax/temporary_object_issue_1037-1220.i
new file mode 100644
index 00000000000..cec72a204fc
--- /dev/null
+++ b/tests/syntax/temporary_object_issue_1037-1220.i
@@ -0,0 +1,93 @@
+/* run.config
+ STDOPT:
+*/
+
+struct X {
+ int arr[1];
+};
+
+struct S {
+ struct X x;
+};
+
+
+struct X get_x(void) { return (struct X){42}; }
+
+struct S get_s(void) { return (struct S){ (struct X){42} }; }
+
+int init(void) {
+ int *p = get_x().arr; // OK
+ p = get_x().arr; // OK
+ int const *q = get_x().arr; // OK
+ return *p + *q; // UB
+}
+
+int g1(int* x) { return *x; }
+void g2(int* x) { *x = 1; }
+
+//from issue 1220
+void calls(void) {
+ // C99: UB access to a[0] in g1 whose lifetime ended
+ // at the sequence point at the start of g1
+ // C11: OK, d is 2.0
+ int d = g1(get_x().arr); // OK
+
+ // C99: UB modification of a[0] whose lifetime ended at the sequence point
+ // C11: UB attempt to modify a temporary object
+ g2(get_x().arr); // OK
+
+ return;
+}
+
+int* cond(void) {
+
+ if(get_x().arr);
+ if((char*)get_x().arr) return 1; // OK
+ if(*(get_x().arr + 0)) return 2; // OK
+
+
+ for (int i = 0; get_x().arr; i++); // OK
+ do{} while (get_x().arr); // OK
+
+ return get_x().arr; // OK
+}
+
+int paren_return(void){
+
+ get_x().arr; // OK
+ (get_x().arr); // OK
+
+ if((get_x().arr)) return 1; //OK
+
+ return *(get_x().arr + 0); // OK
+}
+
+int nested(void){
+ int *p = get_s().x.arr; //OK
+ if((get_s().x.arr)) return 1; // OK
+ int d = g1(get_s().x.arr); // OK
+ return *p; // UB
+}
+
+int f() {return 1;}
+
+int comma(void){
+ int *p;
+ int *q;
+ int x = (p = get_x().arr, *p); //OK
+ int y = *p; // UB
+
+ if((p = get_x().arr, q = get_x().arr, *p + *q)) { //OK
+ return *p + *q; // UB
+ }
+
+ while((p = get_x().arr, *p)) { // OK
+ return *p; // UB
+ }
+ while((p = get_x().arr, *p) && f()){ //OK
+ return *p; //UB
+ }
+ int d = (p = get_x().arr, *p) && *p; // OK
+
+ return y;
+}
--
GitLab