Skip to content

Commit 24c5400

Browse files
committed
Re-add removed broken-crash test as broken-proof
rems-project/cerberus#602 changed the behaviour of this test
1 parent caab64a commit 24c5400

File tree

1 file changed

+48
-0
lines changed
  • src/example-archive/java_program_verification_challenges/broken/error-proof

1 file changed

+48
-0
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
// Tags: main, pointers, structs, alias, java, malloc
2+
3+
//#include <stdio.h>
4+
#include <stdlib.h>
5+
6+
// Struct corresponding to the Java class C
7+
typedef struct C {
8+
struct C *a; // Pointer to same struct type to mimic object reference
9+
int i;
10+
} C;
11+
12+
/* Normal-behavior
13+
* @ requires true;
14+
* @ assignable a, i;
15+
* @ ensures a == NULL && i == 1;
16+
*/
17+
C* createC() {
18+
C* c = (C*) malloc(sizeof(C)); // Allocate memory for C
19+
c->a = NULL; // Initialize as null
20+
c->i = 1; // Initialize i to 1
21+
return c;
22+
}
23+
24+
// Struct corresponding to the Java class Alias
25+
/* typedef struct Alias { */
26+
/* // No direct fields needed */
27+
/* } Alias; */
28+
29+
/* Normal-behavior
30+
* @ requires true;
31+
* @ assignable nothing;
32+
* @ ensures result == 4;
33+
*/
34+
int m() {
35+
C* c = createC(); // Similar to 'C c = new C();'
36+
c->a = c; // Alias to itself
37+
c->i = 2; // Change i to 2
38+
int result = c->i + c->a->i; // Equivalent to 'return c.i + c.a.i;'
39+
free(c); // Clean up allocated memory
40+
return result;
41+
}
42+
43+
int main() {
44+
/* Alias alias; // Instantiate Alias */
45+
int result = m(); // Call m and store result
46+
//printf("Result: %d\n", result); // Print the result
47+
return result;
48+
}

0 commit comments

Comments
 (0)