Yiannis128
commented
8 months ago The following code (FormAI_58452.c) also produces a crash:
ESBMC version 7.4.0 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
Parsing /home/yiannis/git/formai/DATASETSUB/FormAI_58452.c
Converting
Generating GOTO Program
GOTO program creation time: 0.051s
GOTO program processing time: 0.001s
Starting Bounded Model Checking
Not unwinding loop 35 iteration 1 file FormAI_58452.c line 30 column 5 function main
Not unwinding loop 34 iteration 1 file FormAI_58452.c line 16 column 5 function printRooms
Not unwinding loop 36 iteration 1 file FormAI_58452.c line 59 column 17 function main
Not unwinding loop 37 iteration 1 file FormAI_58452.c line 82 column 17 function main
Not unwinding loop 38 iteration 1 file FormAI_58452.c line 38 column 5 function main
Symex completed in: 0.002s (114 assignments)
Slicing time: 0.000s (removed 42 assignments)
Generated 31 VCC(s), 23 remaining after simplification (72 assignments)
No solver specified; defaulting to Boolector
Slicing for Claim arithmetic overflow on add (0.000s)
Slicing time: 0.000s (removed 42 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic//FormAI DATASET v1.0 Category: Hotel Management System ; Style: relaxed
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
// Structure for each room's details.
struct Room {
char name[20];
int roomNumber;
int occupancy;
};
// Function to print available rooms.
void printRooms(struct Room rooms[], int numRooms) {
printf("List of available rooms: \n");
for (int i = 0; i < numRooms; i++) {
if (rooms[i].occupancy == 0) {
printf("Room %d: %s \n", rooms[i].roomNumber, rooms[i].name);
}
}
}
int main() {
int numRooms;
printf("Enter the number of rooms in the hotel: ");
scanf("%d", &numRooms);
struct Room rooms[numRooms];
// Get the details of each room from the user.
for (int i = 0; i < numRooms; i++) {
printf("Enter the name and room number for room %d: ", i+1);
scanf("%s %d", &rooms[i].name, &rooms[i].roomNumber);
rooms[i].occupancy = 0; // Set to 0 initially (i.e., room is not occupied).
}
// Main loop of the program.
int choice = 0;
while (choice != 4) {
printf("\nMENU: \n");
printf("1. Check room availability \n");
printf("2. Book a room \n");
printf("3. Check out of a room \n");
printf("4. Exit \n");
printf("Enter your choice (1-4): ");
scanf("%d", &choice);
switch(choice) {
case 1:
printRooms(rooms, numRooms);
break;
case 2:
printf("Enter the room number you wish to book: ");
int roomToBook;
scanf("%d", &roomToBook);
// Find the room with the given room number.
int indexToBook;
for (int i = 0; i < numRooms; i++) {
if (rooms[i].roomNumber == roomToBook) {
indexToBook = i;
break;
}
}
// If the room is available, book it.
if (rooms[indexToBook].occupancy == 0) {
rooms[indexToBook].occupancy = 1;
printf("Room %d has been booked for you. Enjoy your stay!\n", rooms[indexToBook].roomNumber);
} else {
printf("Sorry, the room is already occupied. Please choose a different room.\n");
}
break;
case 3:
printf("Enter the room number you wish to check out of: ");
int roomToCheckOut;
scanf("%d", &roomToCheckOut);
// Find the room with the given room number.
int indexToCheckOut;
for (int i = 0; i < numRooms; i++) {
if (rooms[i].roomNumber == roomToCheckOut) {
indexToCheckOut = i;
break;
}
}
// If the room is occupied, check out and print the bill.
if (rooms[indexToCheckOut].occupancy == 1) {
rooms[indexToCheckOut].occupancy = 0;
int bill = rand() % 500 + 500; // Generate random bill amount between $500-$1000.
printf("Thank you for your stay. Your bill is $%d.\n", bill);
} else {
printf("Sorry, the room is not occupied. Please choose a different room.\n");
}
break;
case 4:
printf("Thank you for using the hotel management system!\n");
break;
default:
printf("Invalid choice. Please try again.\n");
}
}
return 0;
}
lucasccordeiro
fbrausse
Hi, I was running through the FormAI dataset with ESBMC-AI with the following parameters:
esbmc --overflow --memory-leak-check --timeout 30 --unwind 1 --multi-property --no-unwinding-assertions --no-remove-unreachable ~/git/formai/DATASETSUB/FormAI_52349.cI have received the following output (stdout):
There was no stderr output.
The code of the sample is the following: