Skip to content

Commit f2a8d30

Browse files
michael-schwarzmichael-schwarz
committed
Simplify testing and make dune do the diff
1 parent 36bfdb3 commit f2a8d30

File tree

5 files changed

+161
-180
lines changed

5 files changed

+161
-180
lines changed

‎tests/regression/56-witness/66-ghost-alloc-lock.t‎

Lines changed: 133 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,5 +17,136 @@
1717
total memory locations: 4
1818

1919
$ (yamlWitnessStrip < witness.yml) > new-stripped.yml
20-
$ ./compare-ghost-alloc.sh 66-ghost-alloc-stripped.yml new-stripped.yml
21-
The files are the same after renaming the variables.
20+
$ ./strip-ghost-alloc.sh new-stripped.yml
21+
- entry_type: ghost_instrumentation
22+
content:
23+
ghost_variables:
24+
- name: ALLOC_VAR1_LOCKED
25+
scope: global
26+
type: int
27+
initial:
28+
value: "0"
29+
format: c_expression
30+
- name: ALLOC_VAR2_LOCKED
31+
scope: global
32+
type: int
33+
initial:
34+
value: "0"
35+
format: c_expression
36+
- name: multithreaded
37+
scope: global
38+
type: int
39+
initial:
40+
value: "0"
41+
format: c_expression
42+
ghost_updates:
43+
- location:
44+
file_name: 66-ghost-alloc-lock.c
45+
file_hash: $FILE_HASH
46+
line: 10
47+
column: 3
48+
function: t_fun
49+
updates:
50+
- variable: ALLOC_VAR1_LOCKED
51+
value: "1"
52+
format: c_expression
53+
- location:
54+
file_name: 66-ghost-alloc-lock.c
55+
file_hash: $FILE_HASH
56+
line: 13
57+
column: 3
58+
function: t_fun
59+
updates:
60+
- variable: ALLOC_VAR1_LOCKED
61+
value: "0"
62+
format: c_expression
63+
- location:
64+
file_name: 66-ghost-alloc-lock.c
65+
file_hash: $FILE_HASH
66+
line: 14
67+
column: 3
68+
function: t_fun
69+
updates:
70+
- variable: ALLOC_VAR2_LOCKED
71+
value: "1"
72+
format: c_expression
73+
- location:
74+
file_name: 66-ghost-alloc-lock.c
75+
file_hash: $FILE_HASH
76+
line: 17
77+
column: 3
78+
function: t_fun
79+
updates:
80+
- variable: ALLOC_VAR2_LOCKED
81+
value: "0"
82+
format: c_expression
83+
- location:
84+
file_name: 66-ghost-alloc-lock.c
85+
file_hash: $FILE_HASH
86+
line: 28
87+
column: 3
88+
function: main
89+
updates:
90+
- variable: multithreaded
91+
value: "1"
92+
format: c_expression
93+
- location:
94+
file_name: 66-ghost-alloc-lock.c
95+
file_hash: $FILE_HASH
96+
line: 30
97+
column: 3
98+
function: main
99+
updates:
100+
- variable: ALLOC_VAR1_LOCKED
101+
value: "1"
102+
format: c_expression
103+
- location:
104+
file_name: 66-ghost-alloc-lock.c
105+
file_hash: $FILE_HASH
106+
line: 32
107+
column: 3
108+
function: main
109+
updates:
110+
- variable: ALLOC_VAR1_LOCKED
111+
value: "0"
112+
format: c_expression
113+
- location:
114+
file_name: 66-ghost-alloc-lock.c
115+
file_hash: $FILE_HASH
116+
line: 33
117+
column: 3
118+
function: main
119+
updates:
120+
- variable: ALLOC_VAR2_LOCKED
121+
value: "1"
122+
format: c_expression
123+
- location:
124+
file_name: 66-ghost-alloc-lock.c
125+
file_hash: $FILE_HASH
126+
line: 35
127+
column: 3
128+
function: main
129+
updates:
130+
- variable: ALLOC_VAR2_LOCKED
131+
value: "0"
132+
format: c_expression
133+
- entry_type: flow_insensitive_invariant
134+
flow_insensitive_invariant:
135+
string: '! multithreaded || (ALLOC_VAR2_LOCKED || g2 == 0)'
136+
type: assertion
137+
format: C
138+
- entry_type: flow_insensitive_invariant
139+
flow_insensitive_invariant:
140+
string: '! multithreaded || (ALLOC_VAR1_LOCKED || g1 == 0)'
141+
type: assertion
142+
format: C
143+
- entry_type: flow_insensitive_invariant
144+
flow_insensitive_invariant:
145+
string: '! multithreaded || (0 <= g2 && g2 <= 1)'
146+
type: assertion
147+
format: C
148+
- entry_type: flow_insensitive_invariant
149+
flow_insensitive_invariant:
150+
string: '! multithreaded || (0 <= g1 && g1 <= 1)'
151+
type: assertion
152+
format: C

‎tests/regression/56-witness/66-ghost-alloc-stripped.yml‎

Lines changed: 0 additions & 132 deletions
This file was deleted.

‎tests/regression/56-witness/compare-ghost-alloc.sh‎

Lines changed: 0 additions & 45 deletions
This file was deleted.

‎tests/regression/56-witness/dune‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@
2525
(run %{update_suite} apron-unassume-set-tokens -q)))))
2626

2727
(cram
28-
(deps (glob_files *.c) (glob_files ??-*.yml) (glob_files compare-ghost-alloc.sh)))
28+
(deps (glob_files *.c) (glob_files ??-*.yml) (glob_files strip-ghost-alloc.sh)))
2929

3030
(cram
3131
(applies_to 54-witness-lifter-abortUnless)

‎tests/regression/56-witness/strip-ghost-alloc.sh‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
#!/bin/bash
2+
3+
# Check if the correct number of arguments are provided
4+
if [ "$#" -ne 1 ]; then
5+
echo "Usage: $0 <file>"
6+
exit 1
7+
fi
8+
9+
file="$1"
10+
11+
# Function to extract the first and second occurrences of the pattern
12+
extract_variables() {
13+
grep -o -m 2 'alloc_m[0-9]\+_locked' "$1"
14+
}
15+
16+
# Extract variables from the file
17+
var1=$(extract_variables "$file" | sed -n '1p')
18+
var2=$(extract_variables "$file" | sed -n '2p')
19+
20+
# Check if both variables were found
21+
if [ -z "$var1" ] || [ -z "$var2" ]; then
22+
echo "Error: Could not find two occurrences of the pattern 'alloc_m[0-9]+_locked' in the file."
23+
exit 1
24+
fi
25+
26+
# Rename variables and print the modified file to stdout
27+
sed -e "s/\b$var1\b/ALLOC_VAR1_LOCKED/g" -e "s/\b$var2\b/ALLOC_VAR2_LOCKED/g" "$file"

0 commit comments

Comments
 (0)