source: tests/poly-many-arsz.cfa @ d344a63

Last change on this file since d344a63 was f9ad69d, checked in by Michael Brooks <mlbrooks@…>, 4 months ago

Fix #175

  • Property mode set to 100644
File size: 1.4 KB
Line 
1//
2// Cforall Version 1.0.0 Copyright (C) 2023 University of Waterloo
3//
4// The contents of this file are covered under the licence agreement in the
5// file "LICENCE" distributed with Cforall.
6//
7// poly-many-arsz.cfa -- using many built-in array types with concrete sizes
8//
9// Author           : Mike Brooks
10// Created On       : Tue Aug 13 12:00:00 2024
11// Last Modified By :
12// Last Modified On :
13// Update Count     :
14//
15
16// This behaviour was once broken, as trac #175.
17
18forall( T1*, T2* )
19struct mypair {
20    T1 first;
21    T2 second;
22};
23
24void baseline( void ) {
25    printf("baseline\n");
26
27    // no declaration of x
28    // facts that are true of y:
29
30    mypair(char[2], char) y @= {};
31    printf("|y| = %ld\n", sizeof(y));    // 3
32
33    y.second = 0;
34    printf("y.second = %d\n", y.second); // 0
35
36    y.first[1] = 17;
37    printf("y.second = %d\n", y.second); // 0
38}
39
40void withInterference( void ) {
41    printf("with interference\n");
42
43    // adding this declaration of x ...
44    mypair(char[1], char) x @= {};
45    printf("|x| = %ld\n", sizeof(x));    // 2
46
47    // ... must not affect the observed facts of y:
48
49    mypair(char[2], char) y @= {};
50    printf("|y| = %ld\n", sizeof(y));    // 3
51
52    y.second = 0;
53    printf("y.second = %d\n", y.second); // 0
54
55    y.first[1] = 17;
56    printf("y.second = %d\n", y.second); // 0
57}
58
59int main() {
60    baseline();
61    withInterference();
62    return 0;
63}
Note: See TracBrowser for help on using the repository browser.