From a001d9f818cf073a7ddd1d875a76c6512d6a56ed Mon Sep 17 00:00:00 2001
From: Michal Patera <patermi2@fit.cvut.cz>
Date: Sat, 6 May 2023 18:47:11 +0200
Subject: [PATCH] Fixed errors in code.
---
src/dinitz.c | 6 +++---
src/dinitz.h | 18 ++++++------------
src/main.c | 7 +++++--
3 files changed, 14 insertions(+), 17 deletions(-)
diff --git a/src/dinitz.c b/src/dinitz.c
index d340efb..0bf1330 100644
--- a/src/dinitz.c
+++ b/src/dinitz.c
@@ -8,7 +8,7 @@
void insertHead(Node** head_ref, int new_data) {
- Node* new_node = malloc(sizeof(Node));
+ Node* new_node = (Node*) malloc(sizeof(Node));
//@ assert \valid(new_node);
new_node->data = new_data;
new_node->next = (*head_ref);
@@ -91,7 +91,7 @@ double DFS (int cur, int end, double **graph, int *levels, int *visited, double
double dinitzMaxFlow(int nodes, double **graph){
double total = 0;
- int *vertexLevel = malloc(nodes * sizeof(int));
+ int *vertexLevel = (int*) malloc(nodes * sizeof(int));
int *visited;
// Run BFS to check if flow is possible and set the levels of nodes
@@ -103,7 +103,7 @@ double dinitzMaxFlow(int nodes, double **graph){
{
// Initialize visited array
- visited = calloc(nodes, sizeof(int));
+ visited = (int*) calloc(nodes, sizeof(int));
double flow;
/*@ loop invariant 0 <= total;
@ loop assigns flow, total, visited[0..nodes-1], graph[0..nodes-1][0..nodes-1];
diff --git a/src/dinitz.h b/src/dinitz.h
index aced0b4..7d1e7fc 100644
--- a/src/dinitz.h
+++ b/src/dinitz.h
@@ -3,7 +3,7 @@
typedef struct Node {
int data;
- struct Node* next;
+ struct Node *next;
} Node;
@@ -16,7 +16,7 @@ typedef struct Node {
@ allocates *head_ref;
@ assigns *head_ref;
@*/
-void insertHead(Node** head_ref, int new_data);
+void insertHead(Node **head_ref, int new_data);
/*@ requires \valid(head_ref) && *head_ref != \null;
@@ -24,7 +24,7 @@ void insertHead(Node** head_ref, int new_data);
@ frees *head_ref;
@ ensures *head_ref == \old((*head_ref)->next) && !\valid(\old(*head_ref));
@*/
-void popHead(Node** head_ref);
+void popHead(Node **head_ref);
/*@ requires start >= 0 && end >= 0 && end < 300000;
@@ -44,7 +44,7 @@ int BFS(int start, int end, double **graph, int *levels);
@ assigns visited[0..end], graph[0..end][0..end];
@ ensures \result >= 0.0 && (\result > 0.0 ==> (\forall int i; 0 <= i <= end ==> (graph[cur][i] <= \old(graph[cur][i]) && graph[i][cur] >= \old(graph[i][cur]))));
@*/
-double DFS (int cur, int end, double **graph, int *levels, int *visited, double flow);
+double DFS(int cur, int end, double **graph, int *levels, int *visited, double flow);
/*@ axiomatic SumCapacity {
@@ -63,18 +63,12 @@ double DFS (int cur, int end, double **graph, int *levels, int *visited, double
@ result >= -1 && result <= sum_capacity(graph, nodes, nodes - 1);
@*/
-/*@ lemma max_flow_less_than_capacities:
- @ \forall double **graph, integer nodes, integer sink, double max_flow;
- @ 0 <= nodes && nodes <= 300000 && 0 <= sink < nodes ==>
- @ max_flow <= (\sum int i; 0 <= i < nodes; graph[i][sink]);
- @*/
-
/*@ requires nodes > 0 && nodes <= 300000;
- @ requires graph != \null && \forall int i; 0 <= i < nodes ==> \valid(graph[i] + (0..nodes-1));
+ @ requires graph != \null && \forall integer i; 0 <= i < nodes ==> \valid(graph[i] + (0..nodes-1));
@ ensures valid_flow(\result, graph, nodes);
- @ ensures max_flow_less_than_capacities(graph, nodes, nodes - 1, \result);
@ assigns graph[0..nodes-1][0..nodes-1];
@*/
double dinitzMaxFlow(int nodes, double **graph);
+
#endif // DINITZ_H
\ No newline at end of file
diff --git a/src/main.c b/src/main.c
index 1d1faa5..7a6e89b 100644
--- a/src/main.c
+++ b/src/main.c
@@ -1,8 +1,11 @@
#include <stdio.h>
#include <stdlib.h>
+#include <float.h>
+#include <string.h>
#include "dinitz.h"
+
/*@ axiomatic MemoryManagement {
@ logic boolean is_valid_graph(double **graph, integer nodes) reads graph[0][0..nodes-1];
@ axiom valid_graph:
@@ -35,7 +38,7 @@ int readInput( double ***graph)
return -1;
}
- *graph = malloc((nodes) * sizeof(double *));
+ *graph = (double**) malloc((nodes) * sizeof(double *));
if (*graph == NULL){
return -1;
}
@@ -46,7 +49,7 @@ int readInput( double ***graph)
@*/
for (int i = 0; i < (nodes); ++i)
{
- (*graph)[i] = calloc((nodes), sizeof(double));
+ (*graph)[i] = (double*) calloc((nodes), sizeof(double));
if ((*graph)[i] == NULL){
return -1;
}
--
GitLab