From ddb96a61b4c36d536664d26bda2dd993f1c16405 Mon Sep 17 00:00:00 2001
From: quentin vicens <quentin.vicens@student-cs.fr>
Date: Thu, 20 Mar 2025 21:37:45 +0100
Subject: [PATCH] TP1 WIP
---
config/cert_exp_33.c | 15 +++++++----
config/cert_exp_33_realloc.c | 33 +++++++++++++-----------
config/cwe20.c | 46 ++++++++++++++++++++++-----------
config/main.c | 47 ++++++++++++++++++++++++++++++++++
config/main2.c | 49 ++++++++++++++++++++++++++++++++++++
5 files changed, 157 insertions(+), 33 deletions(-)
create mode 100644 config/main.c
create mode 100644 config/main2.c
diff --git a/config/cert_exp_33.c b/config/cert_exp_33.c
index c4fe87d..73e11de 100644
--- a/config/cert_exp_33.c
+++ b/config/cert_exp_33.c
@@ -1,17 +1,22 @@
+#include <stddef.h>
+
void set_flag(int number, int *sign_flag) {
if (NULL == sign_flag) {
return;
}
-
- if (number > 0) {
+
+ /* Account for number being 0 */
+ if (number >= 0) {
*sign_flag = 1;
- } else if (number < 0) {
+ } else {
*sign_flag = -1;
}
+ Frama_C_show_each_set_flag(number, *sign_flag);
}
-
+
int is_negative(int number) {
- int sign;
+ int sign = 0; /* Initialize for defense-in-depth */
set_flag(number, &sign);
+ Frama_C_show_each_is_negative(number, sign);
return sign < 0;
}
diff --git a/config/cert_exp_33_realloc.c b/config/cert_exp_33_realloc.c
index 30cbd3e..c88be6f 100644
--- a/config/cert_exp_33_realloc.c
+++ b/config/cert_exp_33_realloc.c
@@ -1,39 +1,44 @@
+
#include <stdlib.h>
#include <stdio.h>
+#include <string.h>
+
enum { OLD_SIZE = 10, NEW_SIZE = 20 };
-
-int *resize_array(int *array, size_t count) {
- if (0 == count) {
+
+int *resize_array(int *array, size_t old_count, size_t new_count) {
+ if (0 == new_count) {
return 0;
}
-
- int *ret = (int *)realloc(array, count * sizeof(int));
+
+ int *ret = (int *)realloc(array, new_count * sizeof(int));
if (!ret) {
free(array);
return 0;
}
-
+
+ if (new_count > old_count) {
+ memset(ret + old_count, 0, (new_count - old_count) * sizeof(int));
+ }
+
return ret;
}
-
+
void func(void) {
-
+
int *array = (int *)malloc(OLD_SIZE * sizeof(int));
if (0 == array) {
/* Handle error */
- return;
}
-
+
for (size_t i = 0; i < OLD_SIZE; ++i) {
array[i] = i;
}
-
- array = resize_array(array, NEW_SIZE);
+
+ array = resize_array(array, OLD_SIZE, NEW_SIZE);
if (0 == array) {
/* Handle error */
- return;
}
-
+
for (size_t i = 0; i < NEW_SIZE; ++i) {
printf("%d ", array[i]);
}
diff --git a/config/cwe20.c b/config/cwe20.c
index 9a72365..9fc6a0a 100644
--- a/config/cwe20.c
+++ b/config/cwe20.c
@@ -1,7 +1,9 @@
#include <stdio.h>
#include <stdlib.h>
+#include <limits.h>
+
void die(const char* s) {
- printf("%s",s);
+ printf("%s", s);
exit(2);
}
@@ -9,29 +11,45 @@ void die(const char* s) {
typedef int board_square_t;
-/* board dimensions */
-
-int main () {
- int m,n, error;
+int main() {
+ int m, n, error;
board_square_t *board;
+
printf("Please specify the board height: \n");
error = scanf("%d", &m);
- if ( EOF == error ){
- die("No integer passed: Die evil hacker!\n");
+ if (EOF == error || m <= 0 || m > MAX_DIM) {
+ die("Invalid height: Die evil hacker!\n");
}
+
printf("Please specify the board width: \n");
error = scanf("%d", &n);
- if ( EOF == error ){
- die("No integer passed: Die evil hacker!\n");
+ if (EOF == error || n <= 0 || n > MAX_DIM) {
+ die("Invalid width: Die evil hacker!\n");
+ }
+
+ if (m > INT_MAX / n) {
+ die("Integer overflow detected: Die evil hacker!\n");
}
- if ( m > MAX_DIM || n > MAX_DIM ) {
- die("Value too large: Die evil hacker!\n");
+
+ //@ split m;
+ //@ split n;
+
+ board = (board_square_t*) malloc(m * n * sizeof(board_square_t));
+ if (!board) {
+ return 2;
}
- board = (board_square_t*) malloc( m * n * sizeof(board_square_t));
+
for (int i = 0; i < m; i++) {
for (int j = 0; j < n; j++) {
- board[n*i+j] = 0;
+ board[n * i + j] = 0;
}
}
- if (board[(m-1)*n] == 0) return 0; else return 1;
+
+ if (board[(m - 1) * n] == 0) {
+ free(board);
+ return 0;
+ } else {
+ free(board);
+ return 1;
+ }
}
diff --git a/config/main.c b/config/main.c
new file mode 100644
index 0000000..fb39ff9
--- /dev/null
+++ b/config/main.c
@@ -0,0 +1,47 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include "__fc_builtin.h"
+#include "libstring.h"
+
+#define MAX_LEN 255
+
+int main() {
+ string_t *str1, *str2, *result;
+ char buffer1[MAX_LEN + 1];
+ char buffer2[MAX_LEN + 1];
+
+ for (int i = 0; i < MAX_LEN; i++) {
+ buffer1[i] = (char) Frama_C_interval(1, 127);
+ buffer2[i] = (char) Frama_C_interval(1, 127);
+ }
+ Frama_C_show_each_buffer1(buffer1);
+ Frama_C_show_each_buffer2(buffer2);
+
+ buffer1[MAX_LEN] = '\0';
+ buffer2[MAX_LEN] = '\0';
+
+ str1 = string_new(buffer1);
+ if (!str1) return 1;
+
+ str2 = string_new(buffer2);
+ if (!str2) {
+ free(str1);
+ return 1;
+ }
+
+ result = string_concat(str1, str2);
+ if (!result) {
+ free(str1);
+ free(str2);
+ return 1;
+ }
+
+ printf("Concatenated string: %s\n", result->buf);
+
+ free(result);
+ free(str1);
+ free(str2);
+
+ return 0;
+}
diff --git a/config/main2.c b/config/main2.c
new file mode 100644
index 0000000..626cd0f
--- /dev/null
+++ b/config/main2.c
@@ -0,0 +1,49 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include "__fc_builtin.h"
+#include "libstring.h"
+
+#define FIXED_LEN 20
+
+int main() {
+ string_t *str, *old_char, *new_char, *result;
+ char buffer[FIXED_LEN + 1];
+
+ for (int i = 0; i < FIXED_LEN; i++) {
+ buffer[i] = (char) Frama_C_interval(65, 90); // Lettres majuscules A-Z
+ }
+ buffer[FIXED_LEN] = '\0';
+
+ str = string_new(buffer);
+ if (!str) return 1;
+
+ char old_c = (char) Frama_C_interval(65, 90);
+ char new_c = (char) Frama_C_interval(97, 122);
+
+ old_char = string_new(&old_c);
+ new_char = string_new(&new_c);
+
+ if (!old_char || !new_char) {
+ free(str);
+ return 1;
+ }
+
+ result = string_replace(str, old_char, new_char);
+ if (!result) {
+ free(str);
+ free(old_char);
+ free(new_char);
+ return 1;
+ }
+
+ printf("Original: %s\n", str->buf);
+ printf("Replaced: %s\n", result->buf);
+
+ free(result);
+ free(str);
+ free(old_char);
+ free(new_char);
+
+ return 0;
+}
--
GitLab