-
Notifications
You must be signed in to change notification settings - Fork 38
Open
Labels
Description
This line
cerberus/backend/cn/lib/resourceInference.ml
Line 220 in d87e0f1
| let here = Locations.other __LOC__ in |
Gets into an error message here:
14:56 ➜ cerberus git:(cn-html-escape-ampersand) cn verify other_loc.c
[1/2]: single -- fail
[2/2]: tester -- fail
other_loc.c:20:1: error: Missing resource for returning
void single(cluster_t* cluster)
~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~
Resource needed: Cluster(cluster)
other_loc.c:25:10: (arg C2)
which requires: RW<struct cluster_t>(cluster)
other_loc.c:9:8: (arg Cluster)
which requires: RW<signed int>(&cluster->size)
other location (File "backend/cn/lib/resourceInference.ml", line 220, characters 31-38) (arg size) # <--- HERE!
State file: file:///tmp/state__other_loc.c__single.html
other_loc.c:56:9: error: Left-over unused resource 'Alloc(unpack_Cluster7.Cluster.chars)(unpack_Cluster7.A)'
for (int i=0; i<cluster.size; i++)
Though I'm not exactly sure how, and how to fix it.